# Biconditional Elimination

## Theorem

The rule of biconditional elimination is a valid deduction sequent in propositional logic.

### 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

$(1): \quad p \iff q \vdash p \implies q$
$(2): \quad p \iff q \vdash q \implies p$

## Also known as

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