Theorem eeanv

Description: Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v and 19.42v . For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv . (Contributed by NM, 26-Jul-1995)

	Ref	Expression
Assertion	eeanv	$$⊢\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		nfv	$$⊢Ⅎy\phi$$
2		nfv	$$⊢Ⅎx\psi$$
3	1 2	eean	$$⊢\exists x\exists y\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \exists y\psi \right)$$