This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ψ

Proof

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 ψ