Theorem vtocl3gaf

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

	Ref	Expression
Hypotheses	vtocl3gaf.a	|- F/_ x A
	vtocl3gaf.b	|- F/_ y A
	vtocl3gaf.c	|- F/_ z A
	vtocl3gaf.d	|- F/_ y B
	vtocl3gaf.e	|- F/_ z B
	vtocl3gaf.f	|- F/_ z C
	vtocl3gaf.1	|- F/ x ps
	vtocl3gaf.2	|- F/ y ch
	vtocl3gaf.3	|- F/ z th
	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	vtocl3gaf	|- ( ( A e. R /\ B e. S /\ C e. T ) -> th )

Proof

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