Theorem exdistrv

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v and 19.42v . For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv . (Contributed by BJ, 30-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		exdistr	$$⊢\exists x\exists y\left(\phi \wedge \psi \right)\leftrightarrow \exists x\left(\phi \wedge \exists y\psi \right)$$
2		19.41v	$$⊢\exists x\left(\phi \wedge \exists y\psi \right)\leftrightarrow \left(\exists x\phi \wedge \exists y\psi \right)$$
3	1 2	bitri	$$⊢\exists x\exists y\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \exists y\psi \right)$$