Database: If one side of an equivalence holds, then so does the other

Proposition 107: If one side of an equivalence holds, then so does the other (inference rules)

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

Proof: (a): By biconditional elimination, we infer \phi entails \psi . Using the cut rule, we may thus infer \psi holds.

(b): By symmetry of equivalence, \psi \Leftrightarrow \psi holds. Then, by (a), \psi holds. \square

This database entry builds on the following:

  1. Definition: Equivalence
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Theorem: The cut rule
  5. Theorem: Biconditional elimination
  6. Proposition: Symmetry of equivalence