Theorem eeanv

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.)

Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \)
Proof
l0
nfv
nfv
eean l0 _