Es sei ${\displaystyle {}u}$ eine Variable, die weder in einem der ${\displaystyle {}s_{i}}$ noch in einem der ${\displaystyle {}t_{i}}$ vorkommt. Für jedes ${\displaystyle {}i=1,\ldots ,n}$ setzen wir ${\displaystyle {}\alpha _{i}:=ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}us_{i+1}\ldots s_{n}}$. Nach Axiom  (2) ergibt sich daraus

${\displaystyle \vdash s_{i}=t_{i}\rightarrow {\left(\alpha _{i}{\frac {s_{i}}{u}}\rightarrow \alpha _{i}{\frac {t_{i}}{u}}\right)},}$

also

${\displaystyle \vdash s_{i}=t_{i}\rightarrow {\left({\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}\right)}\rightarrow {\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}t_{i}s_{i+1}\ldots s_{n}\right)}\right)}.}$

Da der Vordersatz in der Implikation rechts nach Axiom  (1) ableitbar ist, ergibt eine aussagenlogische Umformulierung

${\displaystyle \vdash s_{i}=t_{i}\rightarrow {\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}t_{i}s_{i+1}\ldots s_{n}\right)}.}$

Diese Ableitbarkeiten gelten auch, wenn man die Vordersätze durch ihre Konjunktion

${\displaystyle (s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})}$

ersetzt. Durch die Transitivität der Implikation ergibt sich daher

${\displaystyle \vdash (s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})\rightarrow {\left(fs_{1}\ldots s_{n}=ft_{1}\ldots t_{n}\right)}.}$