Proposition 33: Given variables x and y together with statements \alpha, \beta, ..., \omega , the variable substitution \big[ (\alpha \wedge \beta \wedge \cdots \wedge \omega) \big| x \to y \big], where we have used iterated conjunction, is given by \big( [\alpha | x \to y] \wedge [\beta | x \to y] \wedge \cdots \wedge [\omega | x \to y] \big).

Proof: We shall argue by structural induction over the definition of iterated conjunctions.

Base cases: For statements \alpha , \beta and \gamma , recall that (\alpha \wedge \beta \wedge \gamma) is shorthand for the conjunction \big( (\alpha \wedge \beta) \wedge \gamma \big) . By definition of variable substitution, this means that \big[ (\alpha \wedge \beta \wedge \gamma) \big| x \to y\big] is given by \Big( \big[ (\alpha \wedge \beta) \big| x \to y \big] \wedge [\gamma | x \to y] \Big). But \big[ (\alpha \wedge \beta) \big| x \to y \big] is given by \big( [\alpha | x \to y] \wedge [\beta | x \to y] \big) , so the above is \Big( \big( [\alpha | x \to y] \wedge [\beta | x \to y] \big) \wedge [\gamma | x \to y] \Big). This is precisely the definition of \big( [\alpha | x \to y] \wedge [\beta | x \to y] \wedge [\gamma|x \to y]\big) .

Inductive step: We take as the induction hypothesis that the desired result is known for the statements \alpha, \beta, ..., \psi , and need to show from this that it is then also known for the statements \alpha, \beta, ..., \psi, \omega . As (\alpha \wedge \beta \wedge \cdots \wedge \psi \wedge \gamma) is given by \big( (\alpha \wedge \beta \wedge \cdots \wedge \psi) \wedge \omega \big), it follows by the definition of variable substitution that \big[ (\alpha \wedge \beta \wedge \cdots \wedge \psi \wedge \omega ) \big| x \to y \big] is given by \Big( \big[ (\alpha \wedge \beta \wedge \cdots \wedge \psi) \big| x \to y \big] \wedge [\omega | x \to y] \Big). Using the induction hypothesis, this is the same as \Big( \big( [\alpha | x \to y] \wedge [\beta | x \to y] \wedge \cdots \wedge [\psi|x \to y] \big) \wedge [\omega | x \to y] \Big), i.e. \big( [\alpha | x \to y] \wedge [\beta | x \to y] \wedge \cdots \wedge [\psi|x \to y] \wedge [\omega | x \to y] \big) . \square