Step |
Hyp |
Ref |
Expression |
1 |
|
3ecoptocl.1 |
|- S = ( ( D X. D ) /. R ) |
2 |
|
3ecoptocl.2 |
|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) ) |
3 |
|
3ecoptocl.3 |
|- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) ) |
4 |
|
3ecoptocl.4 |
|- ( [ <. v , u >. ] R = C -> ( ch <-> th ) ) |
5 |
|
3ecoptocl.5 |
|- ( ( ( x e. D /\ y e. D ) /\ ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ph ) |
6 |
3
|
imbi2d |
|- ( [ <. z , w >. ] R = B -> ( ( A e. S -> ps ) <-> ( A e. S -> ch ) ) ) |
7 |
4
|
imbi2d |
|- ( [ <. v , u >. ] R = C -> ( ( A e. S -> ch ) <-> ( A e. S -> th ) ) ) |
8 |
2
|
imbi2d |
|- ( [ <. x , y >. ] R = A -> ( ( ( ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ph ) <-> ( ( ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ps ) ) ) |
9 |
5
|
3expib |
|- ( ( x e. D /\ y e. D ) -> ( ( ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ph ) ) |
10 |
1 8 9
|
ecoptocl |
|- ( A e. S -> ( ( ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ps ) ) |
11 |
10
|
com12 |
|- ( ( ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ( A e. S -> ps ) ) |
12 |
1 6 7 11
|
2ecoptocl |
|- ( ( B e. S /\ C e. S ) -> ( A e. S -> th ) ) |
13 |
12
|
com12 |
|- ( A e. S -> ( ( B e. S /\ C e. S ) -> th ) ) |
14 |
13
|
3impib |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> th ) |