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

Proof

Step	Hyp	Ref	Expression
1		exdistr	|- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.41v	|- ( E. x ( ph /\ E. y ps ) <-> ( E. x ph /\ E. y ps ) )
3	1 2	bitri	|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )