# Biconditional Elimination

Jump to navigation
Jump to search

## Theorem

The **rule of biconditional elimination** is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.

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

### Proof Rule

- $(1): \quad$ If we can conclude $\phi \iff \psi$, then we may infer $\phi \implies \psi$.
- $(2): \quad$ If we can conclude $\phi \iff \psi$, then we may infer $\psi \implies \phi$.

### Sequent Form

\(\text {(1)}: \quad\) | \(\ds p \iff q\) | \(\vdash\) | \(\ds p \implies q\) | |||||||||||

\(\text {(2)}: \quad\) | \(\ds p \iff q\) | \(\vdash\) | \(\ds q \implies p\) |

## Also known as

Some sources refer to the Biconditional Elimination as the rule of **Biconditional-Conditional**.