Database: Associativity of conjunction

Proposition 46: Associativity of conjunction (inference rule)

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

Proof: Given the premise of either of (a) or (b), we infer using conjunction elimination repeatedly that \phi holds, \psi holds and \xi holds. We then get the desired conclusion in either case using conjunction introduction twice. \square

This database entry builds on the following:

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