Theorem eeeanv 2351

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 2350	. . 3 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
2	1	anbi1i 627	. 2 ⊢ ((∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
3		df-3an 1091	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	exbii 1855	. . . . 5 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒))
5		19.42v 1962	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
6	4, 5	bitri 278	. . . 4 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
7	6	2exbii 1856	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
8		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑦𝜒
9	8	nfex 2323	. . . . 5 ⊢ Ⅎ𝑦∃𝑧𝜒
10	9	19.41 2233	. . . 4 ⊢ (∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
11	10	exbii 1855	. . 3 ⊢ (∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
12		nfv 1922	. . . . 5 ⊢ Ⅎ𝑥𝜒
13	12	nfex 2323	. . . 4 ⊢ Ⅎ𝑥∃𝑧𝜒
14	13	19.41 2233	. . 3 ⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
15	7, 11, 14	3bitri 300	. 2 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
16		df-3an 1091	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
17	2, 15, 16	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1089  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-ex 1788  df-nf 1792

This theorem is referenced by:  eloprabgaOLD  7319