Inference rule 43: Conjunction elimination (inference rule)

Given that the generalized conjunction (\alpha \wedge \beta \wedge \cdots \wedge \omega) holds, we may for any statement \phi among \alpha, \beta, ..., \omega infer that \phi holds: \cfrac{\vdash (\alpha \wedge \beta \wedge \cdots \wedge \omega)}{\vdash \phi}.

Proof: We argue using structural induction over the recursive definition of generalized conjunctions.

Base cases: Suppose we have statements \alpha , \beta and \gamma such that (\alpha \wedge \beta \wedge \gamma) holds. This is short for the conjunction \big( (\alpha \wedge \beta) \wedge \gamma \big) , so using conjunction elimination we infer that (\alpha \wedge \beta) and \gamma holds; using it again, \alpha , \beta and \gamma hold.

Inductive step: We take as the induction hypothesis that the desired result is evident for the premise \vdash (\alpha \wedge \beta \wedge \cdots \wedge \psi) , and want to show it is then also evident for \vdash (\alpha \wedge \beta \wedge \cdots \wedge \psi \wedge \omega) . But if (\alpha \wedge \beta \wedge \cdots \wedge \psi \wedge \omega) holds, for which \big( (\alpha \wedge \beta \wedge \cdots \wedge \psi) \wedge \omega) \big) is short, then conjunction elimination twice gives us that (\alpha \wedge \beta \wedge \cdots \wedge \psi) holds and \omega holds. By our hypothesis, any \phi among \alpha, \beta, ..., \psi holds; since \omega also holds, we conclude that any statement in the list \alpha, \beta, ..., \psi, \omega holds, as desired. \square