Theorem ceqsex6v 2592

Description: Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.)

Hypotheses

Ref	Expression
ceqsex6v.1	⊢ A ∈ V
ceqsex6v.2	⊢ B ∈ V
ceqsex6v.3	⊢ 𝐶 ∈ V
ceqsex6v.4	⊢ 𝐷 ∈ V
ceqsex6v.5	⊢ 𝐸 ∈ V
ceqsex6v.6	⊢ 𝐹 ∈ V
ceqsex6v.7	⊢ (x = A → (φ ↔ ψ))
ceqsex6v.8	⊢ (y = B → (ψ ↔ χ))
ceqsex6v.9	⊢ (z = 𝐶 → (χ ↔ θ))
ceqsex6v.10	⊢ (w = 𝐷 → (θ ↔ τ))
ceqsex6v.11	⊢ (v = 𝐸 → (τ ↔ η))
ceqsex6v.12	⊢ (u = 𝐹 → (η ↔ ζ))

Assertion

Ref	Expression
ceqsex6v	⊢ (∃x∃y∃z∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ζ)

Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,𝐶,y,z,w,v,u   x,𝐷,y,z,w,v,u   x,𝐸,y,z,w,v,u   x,𝐹,y,z,w,v,u   ψ,x   χ,y   θ,z   τ,w   η,v   ζ,u

Allowed substitution hints:   φ(x,y,z,w,v,u)   ψ(y,z,w,v,u)   χ(x,z,w,v,u)   θ(x,y,w,v,u)   τ(x,y,z,v,u)   η(x,y,z,w,u)   ζ(x,y,z,w,v)

Proof of Theorem ceqsex6v

Step	Hyp	Ref	Expression
1		3anass 888	. . . . 5 ⊢ (((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ((x = A ∧ y = B ∧ z = 𝐶) ∧ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)))
2	1	3exbii 1495	. . . 4 ⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)))
3		19.42vvv 1786	. . . 4 ⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)))
4	2, 3	bitri 173	. . 3 ⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)))
5	4	3exbii 1495	. 2 ⊢ (∃x∃y∃z∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)))
6		ceqsex6v.1	. . . 4 ⊢ A ∈ V
7		ceqsex6v.2	. . . 4 ⊢ B ∈ V
8		ceqsex6v.3	. . . 4 ⊢ 𝐶 ∈ V
9		ceqsex6v.7	. . . . . 6 ⊢ (x = A → (φ ↔ ψ))
10	9	anbi2d 437	. . . . 5 ⊢ (x = A → (((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ)))
11	10	3exbidv 1746	. . . 4 ⊢ (x = A → (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ)))
12		ceqsex6v.8	. . . . . 6 ⊢ (y = B → (ψ ↔ χ))
13	12	anbi2d 437	. . . . 5 ⊢ (y = B → (((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ)))
14	13	3exbidv 1746	. . . 4 ⊢ (y = B → (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ)))
15		ceqsex6v.9	. . . . . 6 ⊢ (z = 𝐶 → (χ ↔ θ))
16	15	anbi2d 437	. . . . 5 ⊢ (z = 𝐶 → (((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ)))
17	16	3exbidv 1746	. . . 4 ⊢ (z = 𝐶 → (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ)))
18	6, 7, 8, 11, 14, 17	ceqsex3v 2590	. . 3 ⊢ (∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ))
19		ceqsex6v.4	. . . 4 ⊢ 𝐷 ∈ V
20		ceqsex6v.5	. . . 4 ⊢ 𝐸 ∈ V
21		ceqsex6v.6	. . . 4 ⊢ 𝐹 ∈ V
22		ceqsex6v.10	. . . 4 ⊢ (w = 𝐷 → (θ ↔ τ))
23		ceqsex6v.11	. . . 4 ⊢ (v = 𝐸 → (τ ↔ η))
24		ceqsex6v.12	. . . 4 ⊢ (u = 𝐹 → (η ↔ ζ))
25	19, 20, 21, 22, 23, 24	ceqsex3v 2590	. . 3 ⊢ (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ) ↔ ζ)
26	18, 25	bitri 173	. 2 ⊢ (∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ζ)
27	5, 26	bitri 173	1 ⊢ (∃x∃y∃z∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ζ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553

This theorem is referenced by: (None)