Theorem eeeanv 2326

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 2325	. . 3 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
2	1	anbi1i 623	. 2 ⊢ ((∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
3		df-3an 1082	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	exbii 1830	. . . . 5 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒))
5		19.42v 1932	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
6	4, 5	bitri 276	. . . 4 ⊢ (∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
7	6	2exbii 1831	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
8		nfv 1893	. . . . . 6 ⊢ Ⅎ𝑦𝜒
9	8	nfex 2305	. . . . 5 ⊢ Ⅎ𝑦∃𝑧𝜒
10	9	19.41 2201	. . . 4 ⊢ (∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
11	10	exbii 1830	. . 3 ⊢ (∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
12		nfv 1893	. . . . 5 ⊢ Ⅎ𝑥𝜒
13	12	nfex 2305	. . . 4 ⊢ Ⅎ𝑥∃𝑧𝜒
14	13	19.41 2201	. . 3 ⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
15	7, 11, 14	3bitri 298	. 2 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒))
16		df-3an 1082	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒))
17	2, 15, 16	3bitr4i 304	1 ⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∃wex 1762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-10 2111  ax-11 2125  ax-12 2140

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-ex 1763  df-nf 1767

This theorem is referenced by:  eloprabga  7120