Step |
Hyp |
Ref |
Expression |
1 |
|
vtocl3gaf.a |
|- F/_ x A |
2 |
|
vtocl3gaf.b |
|- F/_ y A |
3 |
|
vtocl3gaf.c |
|- F/_ z A |
4 |
|
vtocl3gaf.d |
|- F/_ y B |
5 |
|
vtocl3gaf.e |
|- F/_ z B |
6 |
|
vtocl3gaf.f |
|- F/_ z C |
7 |
|
vtocl3gaf.1 |
|- F/ x ps |
8 |
|
vtocl3gaf.2 |
|- F/ y ch |
9 |
|
vtocl3gaf.3 |
|- F/ z th |
10 |
|
vtocl3gaf.4 |
|- ( x = A -> ( ph <-> ps ) ) |
11 |
|
vtocl3gaf.5 |
|- ( y = B -> ( ps <-> ch ) ) |
12 |
|
vtocl3gaf.6 |
|- ( z = C -> ( ch <-> th ) ) |
13 |
|
vtocl3gaf.7 |
|- ( ( x e. R /\ y e. S /\ z e. T ) -> ph ) |
14 |
3
|
nfel1 |
|- F/ z A e. R |
15 |
5
|
nfel1 |
|- F/ z B e. S |
16 |
14 15
|
nfan |
|- F/ z ( A e. R /\ B e. S ) |
17 |
16 9
|
nfim |
|- F/ z ( ( A e. R /\ B e. S ) -> th ) |
18 |
12
|
imbi2d |
|- ( z = C -> ( ( ( A e. R /\ B e. S ) -> ch ) <-> ( ( A e. R /\ B e. S ) -> th ) ) ) |
19 |
|
nfv |
|- F/ x z e. T |
20 |
19 7
|
nfim |
|- F/ x ( z e. T -> ps ) |
21 |
|
nfv |
|- F/ y z e. T |
22 |
21 8
|
nfim |
|- F/ y ( z e. T -> ch ) |
23 |
10
|
imbi2d |
|- ( x = A -> ( ( z e. T -> ph ) <-> ( z e. T -> ps ) ) ) |
24 |
11
|
imbi2d |
|- ( y = B -> ( ( z e. T -> ps ) <-> ( z e. T -> ch ) ) ) |
25 |
13
|
3expia |
|- ( ( x e. R /\ y e. S ) -> ( z e. T -> ph ) ) |
26 |
1 2 4 20 22 23 24 25
|
vtocl2gaf |
|- ( ( A e. R /\ B e. S ) -> ( z e. T -> ch ) ) |
27 |
26
|
com12 |
|- ( z e. T -> ( ( A e. R /\ B e. S ) -> ch ) ) |
28 |
6 17 18 27
|
vtoclgaf |
|- ( C e. T -> ( ( A e. R /\ B e. S ) -> th ) ) |
29 |
28
|
impcom |
|- ( ( ( A e. R /\ B e. S ) /\ C e. T ) -> th ) |
30 |
29
|
3impa |
|- ( ( A e. R /\ B e. S /\ C e. T ) -> th ) |