Theorem alcom

Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw when it allows to avoid dependence on [ax-11]. (Contributed by NM, 30-Jun-1993.)

Conclusion
\( \vdash \forall x \, \forall y \, \varphi \leftrightarrow \forall y \, \forall x \, \varphi \)
Proof
l0
ax-11
ax-11
impbii l0 _