Database: Commutativity of conjunction

Proposition 45: Commutativity of conjunction (inference rule)

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

Proof: Using conjunction elimination twice, we infer that \psi holds and that \phi holds. By conjunction introduction, we then infer that \phi \wedge \psi holds. \square

This database entry builds on the following:

  1. Terminology: Inference rule
  2. Definition: Conjunction
  3. Inference rule: Conjunction introduction
  4. Inference rule: Conjunction elimination