Theorem ee4anv

Description: Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv . (Contributed by NM, 31-Jul-1995)

	Ref	Expression
Assertion	ee4anv	$$⊢\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)$$