Theorem vtocl4g

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

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

Proof

Step	Hyp	Ref	Expression
1		vtocl4g.1	|- ( x = A -> ( ph <-> ps ) )
2		vtocl4g.2	|- ( y = B -> ( ps <-> ch ) )
3		vtocl4g.3	|- ( z = C -> ( ch <-> rh ) )
4		vtocl4g.4	|- ( w = D -> ( rh <-> th ) )
5		vtocl4g.5	|- 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 2 5	vtocl2g	|- ( ( A e. Q /\ B e. R ) -> ch )
9	6 7 8	vtocl2g	|- ( ( C e. S /\ D e. T ) -> ( ( A e. Q /\ B e. R ) -> th ) )
10	9	impcom	|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )