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