Theorem 4exdistrv

Description: Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv . (Contributed by BJ, 5-Jan-2023)

	Ref	Expression
Assertion	4exdistrv	|- ( E. x E. z E. y E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	|- ( E. y E. w ( ph /\ ps ) <-> ( E. y ph /\ E. w ps ) )
2	1	2exbii	|- ( E. x E. z E. y E. w ( ph /\ ps ) <-> E. x E. z ( E. y ph /\ E. w ps ) )
3		exdistrv	|- ( E. x E. z ( E. y ph /\ E. w ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )
4	2 3	bitri	|- ( E. x E. z E. y E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )