Theorem excom

Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on [ax-5], [ax-6], [ax-7], [ax-10], [ax-12]. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)

Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists y \, \exists x \, \varphi \)
Proof
alcom
l1
notbii _
\( \vdash \neg \forall x \, \forall y \, \neg \varphi \leftrightarrow \neg \forall y \, \forall x \, \neg \varphi \)
l2
2exnaln
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \neg \forall x \, \forall y \, \neg \varphi \)
2exnaln
\( \vdash \exists y \, \exists x \, \varphi \leftrightarrow \neg \forall y \, \forall x \, \neg \varphi \)
3bitr4i l1 l2 _