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

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 ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ∧ ∃ 𝑧 𝜒 ) )

Proof

Step Hyp Ref Expression
1 eeanv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) )
2 1 anbi1i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) ↔ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
3 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
4 3 exbii ⊢ ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ∃ 𝑧 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
5 19.42v ⊢ ( ∃ 𝑧 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
6 4 5 bitri ⊢ ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
7 6 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
8 nfv ⊢ Ⅎ 𝑦 𝜒
9 8 nfex ⊢ Ⅎ 𝑦 ∃ 𝑧 𝜒
10 9 19.41 ⊢ ( ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) ↔ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
11 10 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
12 nfv ⊢ Ⅎ 𝑥 𝜒
13 12 nfex ⊢ Ⅎ 𝑥 ∃ 𝑧 𝜒
14 13 19.41 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
15 7 11 14 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
16 df-3an ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ∧ ∃ 𝑧 𝜒 ) ↔ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ) ∧ ∃ 𝑧 𝜒 ) )
17 2 15 16 3bitr4i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜓 ∧ ∃ 𝑧 𝜒 ) )