Step |
Hyp |
Ref |
Expression |
1 |
|
shmod.1 |
|- A e. SH |
2 |
|
shmod.2 |
|- B e. SH |
3 |
|
shmod.3 |
|- C e. SH |
4 |
1 2 3
|
shmodsi |
|- ( A C_ C -> ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) |
5 |
|
ineq1 |
|- ( ( A +H B ) = ( A vH B ) -> ( ( A +H B ) i^i C ) = ( ( A vH B ) i^i C ) ) |
6 |
5
|
sseq1d |
|- ( ( A +H B ) = ( A vH B ) -> ( ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) <-> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) ) |
7 |
4 6
|
syl5ib |
|- ( ( A +H B ) = ( A vH B ) -> ( A C_ C -> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) ) |
8 |
7
|
imp |
|- ( ( ( A +H B ) = ( A vH B ) /\ A C_ C ) -> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) |
9 |
2 3
|
shincli |
|- ( B i^i C ) e. SH |
10 |
1 9
|
shsleji |
|- ( A +H ( B i^i C ) ) C_ ( A vH ( B i^i C ) ) |
11 |
8 10
|
sstrdi |
|- ( ( ( A +H B ) = ( A vH B ) /\ A C_ C ) -> ( ( A vH B ) i^i C ) C_ ( A vH ( B i^i C ) ) ) |