Metamath Proof Explorer

Theorem ee4anv

Description: Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv . (Contributed by NM, 31-Jul-1995) Remove disjoint variable conditions on y , z and x , w . (Revised by Eric Schmidt, 26-Oct-2025)

Ref Expression
Assertion ee4anv ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ψ

Proof

Step Hyp Ref Expression
1 excom ⊢ ∃ y ∃ z ∃ w φ ∧ ψ ↔ ∃ z ∃ y ∃ w φ ∧ ψ
2 1 exbii ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ↔ ∃ x ∃ z ∃ y ∃ w φ ∧ ψ
3 eeanv ⊢ ∃ y ∃ w φ ∧ ψ ↔ ∃ y φ ∧ ∃ w ψ
4 3 2exbii ⊢ ∃ x ∃ z ∃ y ∃ w φ ∧ ψ ↔ ∃ x ∃ z ∃ y φ ∧ ∃ w ψ
5 nfv ⊢ Ⅎ z φ
6 5 nfex ⊢ Ⅎ z ∃ y φ
7 nfv ⊢ Ⅎ x ψ
8 7 nfex ⊢ Ⅎ x ∃ w ψ
9 6 8 eean ⊢ ∃ x ∃ z ∃ y φ ∧ ∃ w ψ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ψ
10 2 4 9 3bitri ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ψ