Metamath Proof Explorer


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 )