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

Metamath Proof Explorer

Theorem 4exdistr

Description: Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995) (Proof shortened by Wolf Lammen, 20-Jan-2018)

Ref Expression
Assertion 4exdistr ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ∧ χ ∧ θ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ ∧ ∃ w θ

Proof

Step Hyp Ref Expression
1 19.42v ⊢ ∃ w χ ∧ θ ↔ χ ∧ ∃ w θ
2 1 anbi2i ⊢ φ ∧ ψ ∧ ∃ w χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ ∃ w θ
3 19.42v ⊢ ∃ w φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ ∃ w χ ∧ θ
4 df-3an ⊢ φ ∧ ψ ∧ χ ∧ ∃ w θ ↔ φ ∧ ψ ∧ χ ∧ ∃ w θ
5 2 3 4 3bitr4i ⊢ ∃ w φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ ∃ w θ
6 5 3exbii ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ∧ χ ∧ θ ↔ ∃ x ∃ y ∃ z φ ∧ ψ ∧ χ ∧ ∃ w θ
7 3exdistr ⊢ ∃ x ∃ y ∃ z φ ∧ ψ ∧ χ ∧ ∃ w θ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ ∧ ∃ w θ
8 6 7 bitri ⊢ ∃ x ∃ y ∃ z ∃ w φ ∧ ψ ∧ χ ∧ θ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ ∧ ∃ w θ