Theorem eeeanv 2382

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.)

Assertion

Ref	Expression
eeeanv	⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))

Distinct variable groups:   𝜑,𝑦   𝜑,𝑧   𝜓,𝑥   𝜓,𝑧   𝜒,𝑥   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑧)

Proof of Theorem eeeanv

Step	Hyp	Ref	Expression
1		eeanv 2381	. . 3 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
2	1	anbi1i 635	. 2 ⊢ ((∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
3		df-3an 1105	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	exbii 1878	. . . . 5 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒))
5		19.42v 1983	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
6	4, 5	bitri 278	. . . 4 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
7	6	2exbii 1879	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
8		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑦𝜒
9	8	nfex 2357	. . . . 5 ⊢ Ⅎ𝑦∃𝑧𝜒
10	9	19.41 2271	. . . 4 ⊢ (∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
11	10	exbii 1878	. . 3 ⊢ (∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
12		nfv 1944	. . . . 5 ⊢ Ⅎ𝑥𝜒
13	12	nfex 2357	. . . 4 ⊢ Ⅎ𝑥∃𝑧𝜒
14	13	19.41 2271	. . 3 ⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
15	7, 11, 14	3bitri 300	. 2 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
16		df-3an 1105	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
17	2, 15, 16	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-ex 1810  df-nf 1814

This theorem is referenced by: (None)