Theorem ee4anvOLD

Description: Obsolete version of ee4anv as of 26-Oct-2025. (Contributed by NM, 31-Jul-1995) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ee4anvOLD	$$⊢\exists x\exists y\exists z\exists w\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		excom	$$⊢\exists y\exists z\exists w\left(\phi \wedge \psi \right)\leftrightarrow \exists z\exists y\exists w\left(\phi \wedge \psi \right)$$
2	1	exbii	$$⊢\exists x\exists y\exists z\exists w\left(\phi \wedge \psi \right)\leftrightarrow \exists x\exists z\exists y\exists w\left(\phi \wedge \psi \right)$$
3		eeanv	$$⊢\exists y\exists w\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists y\phi \wedge \exists w\psi \right)$$
4	3	2exbii	$$⊢\exists x\exists z\exists y\exists w\left(\phi \wedge \psi \right)\leftrightarrow \exists x\exists z\left(\exists y\phi \wedge \exists w\psi \right)$$
5		eeanv	$$⊢\exists x\exists z\left(\exists y\phi \wedge \exists w\psi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\psi \right)$$
6	2 4 5	3bitri	$$⊢\exists x\exists y\exists z\exists w\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\psi \right)$$