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

Proof: Recall the notation for negation and conjunction. Using (g) and (f) in the definition of substitution, and that (\phi \Rightarrow \psi) is short for (\phi \wedge \neg \psi) , we get that \big[ (\phi \Rightarrow \psi) \big| x \to y \big] is \neg \big[ (\phi \wedge \neg \psi) \big| x \to y \big] , hence the same as \neg \big( [\phi | x \to y] \wedge [\neg \psi | x \to y] \big), and thus the same as \neg \big( [\phi | x \to y] \wedge \neg [\psi | x \to y] \big), for which \big( [\phi | x \to y] \Rightarrow [\psi | x \to y] \big) is short. \square