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	|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2		nfv	|- F/ x ps
3	1 2	eean	|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )