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 ψ