Metamath Proof Explorer

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


Step Hyp Ref Expression
1 exdistr x y φ ψ x φ y ψ
2 19.41v x φ y ψ x φ y ψ
3 1 2 bitri x y φ ψ x φ y ψ