Theorem excomw

Weak version of excom and biconditional form of excomimw. Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026.)

Hypotheses
excomw.1
\( \vdash x = w \rightarrow (\varphi \leftrightarrow \psi) \)
excomw.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists y \, \exists x \, \varphi \)
Proof
excomw.1
\( \vdash x = w \rightarrow (\varphi \leftrightarrow \psi) \)
l1
excomimw _
excomw.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
excomimw _
impbii l1 _