Theorem excomw

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

	Ref	Expression
Hypotheses	excomw.1	$$⊢x=w\to \left(\phi \leftrightarrow \psi \right)$$
	excomw.2	$$⊢y=z\to \left(\phi \leftrightarrow \chi \right)$$
Assertion	excomw	$$⊢\exists x\exists y\phi \leftrightarrow \exists y\exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		excomw.1	$$⊢x=w\to \left(\phi \leftrightarrow \psi \right)$$
2		excomw.2	$$⊢y=z\to \left(\phi \leftrightarrow \chi \right)$$
3	1	excomimw	$$⊢\exists x\exists y\phi \to \exists y\exists x\phi$$
4	2	excomimw	$$⊢\exists y\exists x\phi \to \exists x\exists y\phi$$
5	3 4	impbii	$$⊢\exists x\exists y\phi \leftrightarrow \exists y\exists x\phi$$