Database: Implication from equivalence

Proposition 106: Implication from equivalence (inference rule)

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

Proof: (a): By biconditional elimination, we infer \phi entails \psi . By conditional introduction, we thus get that (\phi \Rightarrow \psi) holds.

(b): By symmetry of equivalence, we infer that (\psi \Leftrightarrow \phi) holds. By (a), we can then conclude that (\psi \Rightarrow \phi) holds.

This database entry builds on the following:

  1. Definition: Implication
  2. Definition: Equivalence
  3. Terminology: Inference rule
  4. Theorem: Conditional introduction
  5. Theorem: Biconditional elimination
  6. Proposition: Symmetry of equivalence