Theorem vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019) (Proof shortened by Wolf Lammen, 31-May-2025)

	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	3	imbi2d	|- ( z = C -> ( ( ( A e. Q /\ B e. R ) -> ch ) <-> ( ( A e. Q /\ B e. R ) -> rh ) ) )
7	4	imbi2d	|- ( w = D -> ( ( ( A e. Q /\ B e. R ) -> rh ) <-> ( ( A e. Q /\ B e. R ) -> th ) ) )
8	1	imbi2d	|- ( x = A -> ( ( ( z e. S /\ w e. T ) -> ph ) <-> ( ( z e. S /\ w e. T ) -> ps ) ) )
9	2	imbi2d	|- ( y = B -> ( ( ( z e. S /\ w e. T ) -> ps ) <-> ( ( z e. S /\ w e. T ) -> ch ) ) )
10	5	ex	|- ( ( x e. Q /\ y e. R ) -> ( ( z e. S /\ w e. T ) -> ph ) )
11	8 9 10	vtocl2ga	|- ( ( A e. Q /\ B e. R ) -> ( ( z e. S /\ w e. T ) -> ch ) )
12	11	com12	|- ( ( z e. S /\ w e. T ) -> ( ( A e. Q /\ B e. R ) -> ch ) )
13	6 7 12	vtocl2ga	|- ( ( C e. S /\ D e. T ) -> ( ( A e. Q /\ B e. R ) -> th ) )
14	13	impcom	|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )