Proposition 60: Iterated conjunction elimination (inference rule)

Given that the iterated 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 definition of iterated 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 justified for the premise \vdash (\alpha \wedge \beta \wedge \cdots \wedge \psi) , and want to show it is then also justified 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