Metamath Proof Explorer

Theorem ceqsex6v

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

Ref Expression
Hypotheses ceqsex6v.1 ⊢A∈V
ceqsex6v.2 ⊢B∈V
ceqsex6v.3 ⊢C∈V
ceqsex6v.4 ⊢D∈V
ceqsex6v.5 ⊢E∈V
ceqsex6v.6 ⊢F∈V
ceqsex6v.7 ⊢x=A→φ↔ψ
ceqsex6v.8 ⊢y=B→ψ↔χ
ceqsex6v.9 ⊢z=C→χ↔θ
ceqsex6v.10 ⊢w=D→θ↔τ
ceqsex6v.11 ⊢v=E→τ↔η
ceqsex6v.12 ⊢u=F→η↔ζ
Assertion ceqsex6v ⊢∃x∃y∃z∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔ζ

Proof

Step Hyp Ref Expression
1 ceqsex6v.1 ⊢A∈V
2 ceqsex6v.2 ⊢B∈V
3 ceqsex6v.3 ⊢C∈V
4 ceqsex6v.4 ⊢D∈V
5 ceqsex6v.5 ⊢E∈V
6 ceqsex6v.6 ⊢F∈V
7 ceqsex6v.7 ⊢x=A→φ↔ψ
8 ceqsex6v.8 ⊢y=B→ψ↔χ
9 ceqsex6v.9 ⊢z=C→χ↔θ
10 ceqsex6v.10 ⊢w=D→θ↔τ
11 ceqsex6v.11 ⊢v=E→τ↔η
12 ceqsex6v.12 ⊢u=F→η↔ζ
13 3anass ⊢x=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔x=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ
14 13 3exbii ⊢∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ
15 19.42vvv ⊢∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔x=A∧y=B∧z=C∧∃w∃v∃uw=D∧v=E∧u=F∧φ
16 14 15 bitri ⊢∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔x=A∧y=B∧z=C∧∃w∃v∃uw=D∧v=E∧u=F∧φ
17 16 3exbii ⊢∃x∃y∃z∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔∃x∃y∃zx=A∧y=B∧z=C∧∃w∃v∃uw=D∧v=E∧u=F∧φ
18 7 anbi2d ⊢x=A→w=D∧v=E∧u=F∧φ↔w=D∧v=E∧u=F∧ψ
19 18 3exbidv ⊢x=A→∃w∃v∃uw=D∧v=E∧u=F∧φ↔∃w∃v∃uw=D∧v=E∧u=F∧ψ
20 8 anbi2d ⊢y=B→w=D∧v=E∧u=F∧ψ↔w=D∧v=E∧u=F∧χ
21 20 3exbidv ⊢y=B→∃w∃v∃uw=D∧v=E∧u=F∧ψ↔∃w∃v∃uw=D∧v=E∧u=F∧χ
22 9 anbi2d ⊢z=C→w=D∧v=E∧u=F∧χ↔w=D∧v=E∧u=F∧θ
23 22 3exbidv ⊢z=C→∃w∃v∃uw=D∧v=E∧u=F∧χ↔∃w∃v∃uw=D∧v=E∧u=F∧θ
24 1 2 3 19 21 23 ceqsex3v ⊢∃x∃y∃zx=A∧y=B∧z=C∧∃w∃v∃uw=D∧v=E∧u=F∧φ↔∃w∃v∃uw=D∧v=E∧u=F∧θ
25 4 5 6 10 11 12 ceqsex3v ⊢∃w∃v∃uw=D∧v=E∧u=F∧θ↔ζ
26 17 24 25 3bitri ⊢∃x∃y∃z∃w∃v∃ux=A∧y=B∧z=C∧w=D∧v=E∧u=F∧φ↔ζ