Metamath Proof Explorer


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 x z y w φ ψ x y φ z w ψ

Proof

Step Hyp Ref Expression
1 exdistrv y w φ ψ y φ w ψ
2 1 2exbii x z y w φ ψ x z y φ w ψ
3 exdistrv x z y φ w ψ x y φ z w ψ
4 2 3 bitri x z y w φ ψ x y φ z w ψ