Database: Biconditional elimination

Theorem 103: Biconditional elimination (inference rule)

(a) Given that the equivalence \phi \Leftrightarrow \psi holds, we may infer \phi entails \psi : \cfrac{\vdash (\phi \Leftrightarrow \psi)}{\phi \vdash \psi}. (b) Given that the equivalence \phi \Leftrightarrow \psi holds, we may infer \psi entails \phi : \cfrac{\vdash (\phi \Leftrightarrow \psi)}{\psi \vdash \phi}.

Proof: (a): The equivalence \phi \Leftrightarrow \psi is shorthand for the conjunction \big( (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi) \big) of implications. By conjunction elimination, we infer \phi \Rightarrow \psi . Using [99], we may thus infer \phi entails \psi . \square

(b): This follows from commutativity of conjunction together with (a). \square

This database entry builds on the following:

  1. Definition: Conjunction
  2. Definition: Implication
  3. Definition: Equivalence
  4. Terminology: Entailment
  5. Terminology: Inference rule
  6. Inference rule: Conjunction elimination
  7. Proposition: Commutativity of conjunction
  8. Proposition: Reverse of conditional introduction