Theorem alcoms

Swap quantifiers in an antecedent. (Contributed by NM, 11-May-1993.)

Hypothesis
alcoms.1
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall y \, \forall x \, \varphi \rightarrow \psi \)
Proof
l0
ax-11
\( \vdash \forall y \, \forall x \, \varphi \rightarrow \forall x \, \forall y \, \varphi \)
alcoms.1
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \psi \)
syl l0 _