# Definition:Deduction Rule

 It has been suggested that this page or section be merged into Rule of Implication. (Discuss)

## Theorem

Let $\mathcal L$ be the language of propositional logic.

The Deduction Rule is the rule of inference:

From $U, \mathbf A \vdash \mathbf B$, one may infer $U \vdash \mathbf A \implies \mathbf B$

where:

$\mathbf A, \mathbf B$ are WFFs of propositional logic
$U$ is a set of WFFs

For a given proof system, the Deduction Rule can be either a basic rule of inference, or a derived rule.

### Applicable Proof Systems

The Deduction Rule is either a rule of inference or a derived rule for the following proof systems:

This result is known as the Deduction Theorem.

### Notation

In terms of sequents, the Deduction Rule can be denoted as:

$\dfrac{U, \mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$