Theorem vtocl3ga

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995) Reduce axiom usage. (Revised by Gino Giotto, 3-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl3ga.1	|- ( x = A -> ( ph <-> ps ) )
2		vtocl3ga.2	|- ( y = B -> ( ps <-> ch ) )
3		vtocl3ga.3	|- ( z = C -> ( ch <-> th ) )
4		vtocl3ga.4	|- ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
5		eleq1	|- ( x = A -> ( x e. D <-> A e. D ) )
6	5	3anbi1d	|- ( x = A -> ( ( x e. D /\ y e. R /\ z e. S ) <-> ( A e. D /\ y e. R /\ z e. S ) ) )
7	6 1	imbi12d	|- ( x = A -> ( ( ( x e. D /\ y e. R /\ z e. S ) -> ph ) <-> ( ( A e. D /\ y e. R /\ z e. S ) -> ps ) ) )
8		eleq1	|- ( y = B -> ( y e. R <-> B e. R ) )
9	8	3anbi2d	|- ( y = B -> ( ( A e. D /\ y e. R /\ z e. S ) <-> ( A e. D /\ B e. R /\ z e. S ) ) )
10	9 2	imbi12d	|- ( y = B -> ( ( ( A e. D /\ y e. R /\ z e. S ) -> ps ) <-> ( ( A e. D /\ B e. R /\ z e. S ) -> ch ) ) )
11		eleq1	|- ( z = C -> ( z e. S <-> C e. S ) )
12	11	3anbi3d	|- ( z = C -> ( ( A e. D /\ B e. R /\ z e. S ) <-> ( A e. D /\ B e. R /\ C e. S ) ) )
13	12 3	imbi12d	|- ( z = C -> ( ( ( A e. D /\ B e. R /\ z e. S ) -> ch ) <-> ( ( A e. D /\ B e. R /\ C e. S ) -> th ) ) )
14	7 10 13 4	vtocl3g	|- ( ( A e. D /\ B e. R /\ C e. S ) -> ( ( A e. D /\ B e. R /\ C e. S ) -> th ) )
15	14	pm2.43i	|- ( ( A e. D /\ B e. R /\ C e. S ) -> th )