Metamath Proof Explorer

Theorem eeeanv

Description: Distribute three existential quantifiers over a conjunction. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 25-May-2011) Reduce distinct variable restrictions. (Revised by Wolf Lammen, 20-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 eeanv ⊢ ∃ x ∃ y φ ∧ ψ ↔ ∃ x φ ∧ ∃ y ψ
2 1 anbi1i ⊢ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ
3 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
4 3 exbii ⊢ ∃ z φ ∧ ψ ∧ χ ↔ ∃ z φ ∧ ψ ∧ χ
5 19.42v ⊢ ∃ z φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ ∃ z χ
6 4 5 bitri ⊢ ∃ z φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ ∃ z χ
7 6 2exbii ⊢ ∃ x ∃ y ∃ z φ ∧ ψ ∧ χ ↔ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ
8 nfv ⊢ Ⅎ y χ
9 8 nfex ⊢ Ⅎ y ∃ z χ
10 9 19.41 ⊢ ∃ y φ ∧ ψ ∧ ∃ z χ ↔ ∃ y φ ∧ ψ ∧ ∃ z χ
11 10 exbii ⊢ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ ↔ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ
12 nfv ⊢ Ⅎ x χ
13 12 nfex ⊢ Ⅎ x ∃ z χ
14 13 19.41 ⊢ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ ↔ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ
15 7 11 14 3bitri ⊢ ∃ x ∃ y ∃ z φ ∧ ψ ∧ χ ↔ ∃ x ∃ y φ ∧ ψ ∧ ∃ z χ
16 df-3an ⊢ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ
17 2 15 16 3bitr4i ⊢ ∃ x ∃ y ∃ z φ ∧ ψ ∧ χ ↔ ∃ x φ ∧ ∃ y ψ ∧ ∃ z χ