Proposition 23: Recall \vee denotes disjunction. Given variables x and y and statements \phi and \psi , the variable substitution \big[ (\phi \vee \psi) \big| x \to y \big] is given by \big( [\phi | x \to y] \vee [\psi | x \to y] \big).

Proof: Using the notation for negation and conjunction, (\phi \vee \psi) is short for \neg (\neg \phi \vee \neg \psi) ; using (g) in the definition of substitution, \big[(\phi \vee \psi) \big| x \to y \big] is the same as \neg \big[(\neg \phi \vee \neg \psi) \big| x \to y\big] . By (f) in the definition, this is \neg \big( [\neg \phi|x \to y] \wedge [\neg \psi | x \to y] \big). Using (g) again, this is then the same as \neg \big( \neg [\phi | x \to y] \wedge \neg [\psi | x \to y] \big), for which \big([\phi | x \to y] \vee [\psi | x \to y]\big) is short.