Database: The exchange rule

Theorem 82: The exchange rule (inference rule)

Given that the conjunction \phi \wedge \psi entails \xi , we may infer that the conjunction \psi \wedge \phi entails \xi : \cfrac{(\phi \wedge \psi) \vdash \xi}{(\psi \wedge \phi) \vdash \xi}.

Proof: Assume \psi \wedge \phi . By commutativity of conjunction, we infer that \phi \wedge \psi holds. But then, using the cut rule, we infer that \xi holds. This has showed that \psi \wedge \phi entails \xi . \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Conjunction
  3. Terminology: Inference
  4. Terminology: Entailment
  5. Terminology: Inference rule
  6. Proposition: Commutativity of conjunction
  7. Theorem: The cut rule