Step |
Hyp |
Ref |
Expression |
1 |
|
pjoml2.1 |
|- A e. CH |
2 |
|
pjoml2.2 |
|- B e. CH |
3 |
1 2
|
chincli |
|- ( A i^i B ) e. CH |
4 |
2
|
choccli |
|- ( _|_ ` B ) e. CH |
5 |
1 4
|
chincli |
|- ( A i^i ( _|_ ` B ) ) e. CH |
6 |
3 5
|
chjcomi |
|- ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i B ) ) |
7 |
2
|
pjococi |
|- ( _|_ ` ( _|_ ` B ) ) = B |
8 |
7
|
ineq2i |
|- ( A i^i ( _|_ ` ( _|_ ` B ) ) ) = ( A i^i B ) |
9 |
8
|
oveq2i |
|- ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i B ) ) |
10 |
6 9
|
eqtr4i |
|- ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) |
11 |
10
|
eqeq2i |
|- ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) <-> A = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) ) |
12 |
1 2
|
cmbri |
|- ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) |
13 |
1 4
|
cmbri |
|- ( A C_H ( _|_ ` B ) <-> A = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) ) |
14 |
11 12 13
|
3bitr4i |
|- ( A C_H B <-> A C_H ( _|_ ` B ) ) |