Step |
Hyp |
Ref |
Expression |
1 |
|
cmcm3 |
|- ( ( B e. CH /\ A e. CH ) -> ( B C_H A <-> ( _|_ ` B ) C_H A ) ) |
2 |
1
|
ancoms |
|- ( ( A e. CH /\ B e. CH ) -> ( B C_H A <-> ( _|_ ` B ) C_H A ) ) |
3 |
|
cmcm |
|- ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> B C_H A ) ) |
4 |
|
choccl |
|- ( B e. CH -> ( _|_ ` B ) e. CH ) |
5 |
|
cmcm |
|- ( ( A e. CH /\ ( _|_ ` B ) e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( _|_ ` B ) C_H A ) ) |
6 |
4 5
|
sylan2 |
|- ( ( A e. CH /\ B e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( _|_ ` B ) C_H A ) ) |
7 |
2 3 6
|
3bitr4d |
|- ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> A C_H ( _|_ ` B ) ) ) |