Theorem vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019)

	Ref	Expression
Hypotheses	vtocl4ga.1	|- ( x = A -> ( ph <-> ps ) )
	vtocl4ga.2	|- ( y = B -> ( ps <-> ch ) )
	vtocl4ga.3	|- ( z = C -> ( ch <-> rh ) )
	vtocl4ga.4	|- ( w = D -> ( rh <-> th ) )
	vtocl4ga.5	|- ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph )
Assertion	vtocl4ga	|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )

Proof

Step	Hyp	Ref	Expression
1		vtocl4ga.1	|- ( x = A -> ( ph <-> ps ) )
2		vtocl4ga.2	|- ( y = B -> ( ps <-> ch ) )
3		vtocl4ga.3	|- ( z = C -> ( ch <-> rh ) )
4		vtocl4ga.4	|- ( w = D -> ( rh <-> th ) )
5		vtocl4ga.5	|- ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph )
6		eleq1	|- ( x = A -> ( x e. Q <-> A e. Q ) )
7	6	anbi1d	|- ( x = A -> ( ( x e. Q /\ y e. R ) <-> ( A e. Q /\ y e. R ) ) )
8	7	anbi1d	|- ( x = A -> ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) ) )
9	8 1	imbi12d	|- ( x = A -> ( ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph ) <-> ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ps ) ) )
10		eleq1	|- ( y = B -> ( y e. R <-> B e. R ) )
11	10	anbi2d	|- ( y = B -> ( ( A e. Q /\ y e. R ) <-> ( A e. Q /\ B e. R ) ) )
12	11	anbi1d	|- ( y = B -> ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) ) )
13	12 2	imbi12d	|- ( y = B -> ( ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ps ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) -> ch ) ) )
14		eleq1	|- ( z = C -> ( z e. S <-> C e. S ) )
15	14	anbi1d	|- ( z = C -> ( ( z e. S /\ w e. T ) <-> ( C e. S /\ w e. T ) ) )
16	15	anbi2d	|- ( z = C -> ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) ) )
17	16 3	imbi12d	|- ( z = C -> ( ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) -> ch ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) -> rh ) ) )
18		eleq1	|- ( w = D -> ( w e. T <-> D e. T ) )
19	18	anbi2d	|- ( w = D -> ( ( C e. S /\ w e. T ) <-> ( C e. S /\ D e. T ) ) )
20	19	anbi2d	|- ( w = D -> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) ) )
21	20 4	imbi12d	|- ( w = D -> ( ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) -> rh ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th ) ) )
22	9 13 17 21 5	vtocl4g	|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th ) )
23	22	pm2.43i	|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )