# Rule of Implication

## Proof Rule

The rule of implication is a valid argument in types of logic dealing with conditionals $\implies$.

This includes propositional logic and predicate logic, and in particular natural deduction.

### Proof Rule

If, by making an assumption $\phi$, we can conclude $\psi$ as a consequence, we may infer $\phi \implies \psi$.
The conclusion $\phi \implies \psi$ does not depend on the assumption $\phi$, which is thus discharged.

### Sequent Form

The Rule of Implication can be symbolised by the sequent:

 $\ds \paren {p \vdash q}$  $\ds$ $\ds \vdash \ \$ $\ds p \implies q$  $\ds$

## Explanation

The Rule of Implication can be expressed in natural language as:

If by making an assumption $\phi$ we can deduce $\psi$, then we can encapsulate this deduction into the compound statement $\phi \implies \psi$.

## Also known as

The Rule of Implication is sometimes known as:

• The rule of implies-introduction
• The rule of conditional proof (abbreviated $\text{CP}$).