Database: Symmetry of equivalence

Proposition 104: Symmetry of equivalence (inference rule)

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

Proof: Using biconditional elimination twice, we infer that \psi entails \phi and \phi entails \psi . By biconditional introduction, we infer \psi \Leftrightarrow \phi holds. \square

This database entry builds on the following:

  1. Definition: Equivalence
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Theorem: Biconditional introduction
  5. Theorem: Biconditional elimination