Step |
Hyp |
Ref |
Expression |
1 |
|
shjshs.1 |
|- A e. SH |
2 |
|
shjshs.2 |
|- B e. SH |
3 |
1 2
|
shjshsi |
|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) ) |
4 |
|
ococ |
|- ( ( A +H B ) e. CH -> ( _|_ ` ( _|_ ` ( A +H B ) ) ) = ( A +H B ) ) |
5 |
3 4
|
eqtr2id |
|- ( ( A +H B ) e. CH -> ( A +H B ) = ( A vH B ) ) |
6 |
1 2
|
shjcli |
|- ( A vH B ) e. CH |
7 |
|
eleq1 |
|- ( ( A +H B ) = ( A vH B ) -> ( ( A +H B ) e. CH <-> ( A vH B ) e. CH ) ) |
8 |
6 7
|
mpbiri |
|- ( ( A +H B ) = ( A vH B ) -> ( A +H B ) e. CH ) |
9 |
5 8
|
impbii |
|- ( ( A +H B ) e. CH <-> ( A +H B ) = ( A vH B ) ) |