Biconditional Elimination

From ProofWiki
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.


Also see