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 ) |