Step |
Hyp |
Ref |
Expression |
1 |
|
sseq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A C_ B <-> if ( A e. CH , A , 0H ) C_ B ) ) |
2 |
|
breq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A C_H B <-> if ( A e. CH , A , 0H ) C_H B ) ) |
3 |
1 2
|
imbi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( A C_ B -> A C_H B ) <-> ( if ( A e. CH , A , 0H ) C_ B -> if ( A e. CH , A , 0H ) C_H B ) ) ) |
4 |
|
sseq2 |
|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C_ B <-> if ( A e. CH , A , 0H ) C_ if ( B e. CH , B , 0H ) ) ) |
5 |
|
breq2 |
|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C_H B <-> if ( A e. CH , A , 0H ) C_H if ( B e. CH , B , 0H ) ) ) |
6 |
4 5
|
imbi12d |
|- ( B = if ( B e. CH , B , 0H ) -> ( ( if ( A e. CH , A , 0H ) C_ B -> if ( A e. CH , A , 0H ) C_H B ) <-> ( if ( A e. CH , A , 0H ) C_ if ( B e. CH , B , 0H ) -> if ( A e. CH , A , 0H ) C_H if ( B e. CH , B , 0H ) ) ) ) |
7 |
|
h0elch |
|- 0H e. CH |
8 |
7
|
elimel |
|- if ( A e. CH , A , 0H ) e. CH |
9 |
7
|
elimel |
|- if ( B e. CH , B , 0H ) e. CH |
10 |
8 9
|
lecmi |
|- ( if ( A e. CH , A , 0H ) C_ if ( B e. CH , B , 0H ) -> if ( A e. CH , A , 0H ) C_H if ( B e. CH , B , 0H ) ) |
11 |
3 6 10
|
dedth2h |
|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B -> A C_H B ) ) |
12 |
11
|
3impia |
|- ( ( A e. CH /\ B e. CH /\ A C_ B ) -> A C_H B ) |