Theorem excomimw
Weak version of excomim. Uses only Tarski's FOL axiom schemes.
(Contributed by BTernaryTau, 23-Jun-2025.)
Hypothesis
excomimw.1
\( \vdash x = z \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \rightarrow \exists y \, \exists x \, \varphi \)
Proof
excomimw.1
notbid _
\( \vdash x = z \rightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
alcomimw _
l3
con3i _
\( \vdash \neg \forall x \, \forall y \, \neg \varphi \rightarrow \neg \forall y \, \forall x \, \neg \varphi \)
l4
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 \)
3imtr4i l3 l4 _