Database: Transitivity of implication

Proposition: Transitivity of implication (inference rule)

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

Proof: Using [99] twice, infer that \phi entails \psi and that \psi entails \xi . Then, by transitivity of entailment, we infer \phi entails \xi . Finally, we get by conditional introduction that \phi \Rightarrow \xi holds. \square

This database entry builds on the following:

  1. Definition: Implication
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Theorem: Conditional introduction
  5. Proposition: Transitivity of entailment
  6. Proposition: Reverse of conditional introduction