Theorem 4exdistrv

Description: Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv . (Contributed by BJ, 5-Jan-2023)

	Ref	Expression
Assertion	4exdistrv	$$⊢\exists x\exists z\exists y\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		exdistrv	$$⊢\exists y\exists w\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists y\phi \wedge \exists w\psi \right)$$
2	1	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)$$
3		exdistrv	$$⊢\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)$$
4	2 3	bitri	$$⊢\exists x\exists z\exists y\exists w\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\psi \right)$$