Biconditional Elimination

From ProofWiki
Jump to navigation Jump to search

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.


Also see