Database: Conjunction elimination

Inference rule 42: Conjunction elimination (declared)

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

This database entry builds on the following:

  1. Terminology: Inference rule
  2. Definition: Conjunction