Theorem ax12vALT

Alternate proof of ax12v2, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)

Conclusion
\( \vdash x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
ax-1
\( \vdash \varphi \rightarrow x = y' \rightarrow \varphi \)
axc16
\( \vdash \forall x \, x = y' \rightarrow (x = y' \rightarrow \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
syl5 l0 _
l3
a1d _
\( \vdash \forall x \, x = y' \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
axc15
\( \vdash \neg \forall x \, x = y' \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
pm2.61i l3 _