Theorem bj-alcomexcom

Description: Commutation of universal quantifiers implies commutation of existential quantifiers. Can be placed in the ax-4 section, soon after 2nexaln , and used to prove excom . (Contributed by BJ, 29-Nov-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-alcomexcom	$$⊢\left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)\to \left(\exists y\exists x\phi \to \exists x\exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		2nexaln	$$⊢\neg \exists x\exists y\phi \leftrightarrow \forall x\forall y\neg \phi$$
2		2nexaln	$$⊢\neg \exists y\exists x\phi \leftrightarrow \forall y\forall x\neg \phi$$
3	1 2	imbi12i	$$⊢\left(\neg \exists x\exists y\phi \to \neg \exists y\exists x\phi \right)\leftrightarrow \left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)$$
4		con4	$$⊢\left(\neg \exists x\exists y\phi \to \neg \exists y\exists x\phi \right)\to \left(\exists y\exists x\phi \to \exists x\exists y\phi \right)$$
5	3 4	sylbir	$$⊢\left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)\to \left(\exists y\exists x\phi \to \exists x\exists y\phi \right)$$