Theorem vtocl3gaf 2923

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
vtocl3gaf.a	|- F/_xA
vtocl3gaf.b	|- F/_yA
vtocl3gaf.c	|- F/_zA
vtocl3gaf.d	|- F/_yB
vtocl3gaf.e	|- F/_zB
vtocl3gaf.f	|- F/_zC
vtocl3gaf.1	|- F/xps
vtocl3gaf.2	|- F/ych
vtocl3gaf.3	|- F/zth
vtocl3gaf.4	|- (x = A -> (ph <-> ps))
vtocl3gaf.5	|- (y = B -> (ps <-> ch))
vtocl3gaf.6	|- (z = C -> (ch <-> th))
vtocl3gaf.7	|- ((x e. R /\ y e. S /\ z e. T) -> ph)

Assertion

Ref	Expression
vtocl3gaf	|- ((A e. R /\ B e. S /\ C e. T) -> th)

Distinct variable groups:   x,y,z,R   x,S,y,z   x,T,y,z

Allowed substitution hints:   ph(x,y,z)   ps(x,y,z)   ch(x,y,z)   th(x,y,z)   A(x,y,z)   B(x,y,z)   C(x,y,z)

Proof of Theorem vtocl3gaf

Step	Hyp	Ref	Expression
1		vtocl3gaf.a	. . 3 |- F/_xA
2		vtocl3gaf.b	. . 3 |- F/_yA
3		vtocl3gaf.c	. . 3 |- F/_zA
4		vtocl3gaf.d	. . 3 |- F/_yB
5		vtocl3gaf.e	. . 3 |- F/_zB
6		vtocl3gaf.f	. . 3 |- F/_zC
7	1	nfel1 2499	. . . . 5 |- F/x A e. R
8		nfv 1619	. . . . 5 |- F/x y e. S
9		nfv 1619	. . . . 5 |- F/x z e. T
10	7, 8, 9	nf3an 1827	. . . 4 |- F/x(A e. R /\ y e. S /\ z e. T)
11		vtocl3gaf.1	. . . 4 |- F/xps
12	10, 11	nfim 1813	. . 3 |- F/x((A e. R /\ y e. S /\ z e. T) -> ps)
13	2	nfel1 2499	. . . . 5 |- F/y A e. R
14	4	nfel1 2499	. . . . 5 |- F/y B e. S
15		nfv 1619	. . . . 5 |- F/y z e. T
16	13, 14, 15	nf3an 1827	. . . 4 |- F/y(A e. R /\ B e. S /\ z e. T)
17		vtocl3gaf.2	. . . 4 |- F/ych
18	16, 17	nfim 1813	. . 3 |- F/y((A e. R /\ B e. S /\ z e. T) -> ch)
19	3	nfel1 2499	. . . . 5 |- F/z A e. R
20	5	nfel1 2499	. . . . 5 |- F/z B e. S
21	6	nfel1 2499	. . . . 5 |- F/z C e. T
22	19, 20, 21	nf3an 1827	. . . 4 |- F/z(A e. R /\ B e. S /\ C e. T)
23		vtocl3gaf.3	. . . 4 |- F/zth
24	22, 23	nfim 1813	. . 3 |- F/z((A e. R /\ B e. S /\ C e. T) -> th)
25		eleq1 2413	. . . . 5 |- (x = A -> (x e. R <-> A e. R))
26	25	3anbi1d 1256	. . . 4 |- (x = A -> ((x e. R /\ y e. S /\ z e. T) <-> (A e. R /\ y e. S /\ z e. T)))
27		vtocl3gaf.4	. . . 4 |- (x = A -> (ph <-> ps))
28	26, 27	imbi12d 311	. . 3 |- (x = A -> (((x e. R /\ y e. S /\ z e. T) -> ph) <-> ((A e. R /\ y e. S /\ z e. T) -> ps)))
29		eleq1 2413	. . . . 5 |- (y = B -> (y e. S <-> B e. S))
30	29	3anbi2d 1257	. . . 4 |- (y = B -> ((A e. R /\ y e. S /\ z e. T) <-> (A e. R /\ B e. S /\ z e. T)))
31		vtocl3gaf.5	. . . 4 |- (y = B -> (ps <-> ch))
32	30, 31	imbi12d 311	. . 3 |- (y = B -> (((A e. R /\ y e. S /\ z e. T) -> ps) <-> ((A e. R /\ B e. S /\ z e. T) -> ch)))
33		eleq1 2413	. . . . 5 |- (z = C -> (z e. T <-> C e. T))
34	33	3anbi3d 1258	. . . 4 |- (z = C -> ((A e. R /\ B e. S /\ z e. T) <-> (A e. R /\ B e. S /\ C e. T)))
35		vtocl3gaf.6	. . . 4 |- (z = C -> (ch <-> th))
36	34, 35	imbi12d 311	. . 3 |- (z = C -> (((A e. R /\ B e. S /\ z e. T) -> ch) <-> ((A e. R /\ B e. S /\ C e. T) -> th)))
37		vtocl3gaf.7	. . 3 |- ((x e. R /\ y e. S /\ z e. T) -> ph)
38	1, 2, 3, 4, 5, 6, 12, 18, 24, 28, 32, 36, 37	vtocl3gf 2917	. 2 |- ((A e. R /\ B e. S /\ C e. T) -> ((A e. R /\ B e. S /\ C e. T) -> th))
39	38	pm2.43i 43	1 |- ((A e. R /\ B e. S /\ C e. T) -> th)

Syntax hints:   -> wi 4   <-> wb 176   /\ w3a 934   F/wnf 1544   = wceq 1642   e. wcel 1710   F/_wnfc 2476

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-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  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-nfc 2478  df-v 2861

This theorem is referenced by:  vtocl3ga  2924