Theorem ceqsex6v 2900

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

Hypotheses

Ref	Expression
ceqsex6v.1	|- A e. _V
ceqsex6v.2	|- B e. _V
ceqsex6v.3	|- C e. _V
ceqsex6v.4	|- D e. _V
ceqsex6v.5	|- E e. _V
ceqsex6v.6	|- F e. _V
ceqsex6v.7	|- (x = A -> (ph <-> ps))
ceqsex6v.8	|- (y = B -> (ps <-> ch))
ceqsex6v.9	|- (z = C -> (ch <-> th))
ceqsex6v.10	|- (w = D -> (th <-> ta))
ceqsex6v.11	|- (v = E -> (ta <-> et))
ceqsex6v.12	|- (u = F -> (et <-> ze))

Assertion

Ref	Expression
ceqsex6v	|- (E.xE.yE.zE.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> ze)

Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,C,y,z,w,v,u   x,D,y,z,w,v,u   x,E,y,z,w,v,u   x,F,y,z,w,v,u   ps,x   ch,y   th,z   ta,w   et,v   ze,u

Allowed substitution hints:   ph(x,y,z,w,v,u)   ps(y,z,w,v,u)   ch(x,z,w,v,u)   th(x,y,w,v,u)   ta(x,y,z,v,u)   et(x,y,z,w,u)   ze(x,y,z,w,v)

Proof of Theorem ceqsex6v

Step	Hyp	Ref	Expression
1		3anass 938	. . . . 5 |- (((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> ((x = A /\ y = B /\ z = C) /\ ((w = D /\ v = E /\ u = F) /\ ph)))
2	1	3exbii 1584	. . . 4 |- (E.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> E.wE.vE.u((x = A /\ y = B /\ z = C) /\ ((w = D /\ v = E /\ u = F) /\ ph)))
3		19.42vvv 1908	. . . 4 |- (E.wE.vE.u((x = A /\ y = B /\ z = C) /\ ((w = D /\ v = E /\ u = F) /\ ph)) <-> ((x = A /\ y = B /\ z = C) /\ E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph)))
4	2, 3	bitri 240	. . 3 |- (E.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> ((x = A /\ y = B /\ z = C) /\ E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph)))
5	4	3exbii 1584	. 2 |- (E.xE.yE.zE.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> E.xE.yE.z((x = A /\ y = B /\ z = C) /\ E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph)))
6		ceqsex6v.1	. . . 4 |- A e. _V
7		ceqsex6v.2	. . . 4 |- B e. _V
8		ceqsex6v.3	. . . 4 |- C e. _V
9		ceqsex6v.7	. . . . . 6 |- (x = A -> (ph <-> ps))
10	9	anbi2d 684	. . . . 5 |- (x = A -> (((w = D /\ v = E /\ u = F) /\ ph) <-> ((w = D /\ v = E /\ u = F) /\ ps)))
11	10	3exbidv 1629	. . . 4 |- (x = A -> (E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph) <-> E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ps)))
12		ceqsex6v.8	. . . . . 6 |- (y = B -> (ps <-> ch))
13	12	anbi2d 684	. . . . 5 |- (y = B -> (((w = D /\ v = E /\ u = F) /\ ps) <-> ((w = D /\ v = E /\ u = F) /\ ch)))
14	13	3exbidv 1629	. . . 4 |- (y = B -> (E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ps) <-> E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ch)))
15		ceqsex6v.9	. . . . . 6 |- (z = C -> (ch <-> th))
16	15	anbi2d 684	. . . . 5 |- (z = C -> (((w = D /\ v = E /\ u = F) /\ ch) <-> ((w = D /\ v = E /\ u = F) /\ th)))
17	16	3exbidv 1629	. . . 4 |- (z = C -> (E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ch) <-> E.wE.vE.u((w = D /\ v = E /\ u = F) /\ th)))
18	6, 7, 8, 11, 14, 17	ceqsex3v 2898	. . 3 |- (E.xE.yE.z((x = A /\ y = B /\ z = C) /\ E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph)) <-> E.wE.vE.u((w = D /\ v = E /\ u = F) /\ th))
19		ceqsex6v.4	. . . 4 |- D e. _V
20		ceqsex6v.5	. . . 4 |- E e. _V
21		ceqsex6v.6	. . . 4 |- F e. _V
22		ceqsex6v.10	. . . 4 |- (w = D -> (th <-> ta))
23		ceqsex6v.11	. . . 4 |- (v = E -> (ta <-> et))
24		ceqsex6v.12	. . . 4 |- (u = F -> (et <-> ze))
25	19, 20, 21, 22, 23, 24	ceqsex3v 2898	. . 3 |- (E.wE.vE.u((w = D /\ v = E /\ u = F) /\ th) <-> ze)
26	18, 25	bitri 240	. 2 |- (E.xE.yE.z((x = A /\ y = B /\ z = C) /\ E.wE.vE.u((w = D /\ v = E /\ u = F) /\ ph)) <-> ze)
27	5, 26	bitri 240	1 |- (E.xE.yE.zE.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> ze)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by: (None)