Database: Transitivity of equivalence

Proposition 105: Transitivity of equivalence (inference rule)

Given that the equivalence \phi \Leftrightarrow \psi holds and that \psi \Leftrightarrow \xi holds, we may infer that \phi \Leftrightarrow \xi holds: \cfrac{\vdash (\phi \Leftrightarrow \psi) \quad \vdash (\psi \Leftrightarrow \xi)}{\vdash (\phi \Leftrightarrow \xi)}.

Proof: Using biconditional elimination twice, we infer that \phi entails \psi and \psi entails \xi . By transitivity of entailment, this means \phi entails \xi . Similarly, using biconditional elimination twice (on the original premises) we infer that that \xi entails \psi and \psi entails \phi . By transitivity of entailment, \xi entails \phi . By biconditional introduction, we therefore conclude \phi \Leftrightarrow \xi holds. \square

This database entry builds on the following:

  1. Definition: Equivalence
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Theorem: Biconditional introduction
  5. Proposition: Transitivity of entailment
  6. Theorem: Biconditional elimination