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

Proof: Recall the notation for implication and conjunction. Since (\phi \Leftrightarrow \psi) is short for \big( (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi) \big) , we get by (f) in the definition of variable substitution that \big[ (\phi \Leftrightarrow \psi) \big| x \to y \big] is the same as \Big( \big[ (\phi \Rightarrow \psi) \big | x \to y \big] \wedge \big[ (\psi \Rightarrow \phi) \big| x \to y \big] \Big), and hence by [24] the same as \Big( \big( [ \phi | x \to y] \Rightarrow [\psi | x \to y] \big) \wedge \big( [ \psi | x \to y] \Rightarrow [\phi | x \to y] \big) \Big), for which \big( [\phi | x \to y] \Leftrightarrow [\psi | x \to y] \big) is short. \square