Database: Contraposition of implication

Proposition: Contraposition of implication (inference rule)

Given that the implication \phi \Rightarrow \psi holds, we may infer that its contrapositive \neg \psi \Rightarrow \neg \phi holds: \cfrac{\vdash (\phi \Rightarrow \psi)}{\vdash (\neg \psi \Rightarrow \neg \phi)}.

Verification: By [99], infer that \phi entails \psi . By [69], infer that \neg \psi entails \neg \phi . By conditional introduction, conclude \neg \psi \Rightarrow \neg \phi holds. \square

This database entry builds on the following:

  1. Definition: Implication
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Proposition: Negation of entailment
  5. Theorem: Conditional introduction
  6. Proposition: Reverse of conditional introduction
  7. Definition: Contrapositive of an implication