Theorem ax11w

Weak version of [ax-11] from which we can prove any [ax-11] instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. Unlike [ax-11], this theorem requires that \( x \) and \( y \) be distinct i.e. are not bundled. It is an alias of alcomimw introduced for labeling consistency. (Contributed by NM, 10-Apr-2017.) Use alcomimw instead. (New usage is discouraged.)

Hypothesis
ax11w.1
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
Proof
ax11w.1
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \psi) \)
alcomimw _