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

Metamath Proof Explorer

Theorem exdistr2

Description: Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995)

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

Proof

Step Hyp Ref Expression
1 19.42vv ⊢ ∃ y ∃ z φ ∧ ψ ↔ φ ∧ ∃ y ∃ z ψ
2 1 exbii ⊢ ∃ x ∃ y ∃ z φ ∧ ψ ↔ ∃ x φ ∧ ∃ y ∃ z ψ