Metamath Proof Explorer
Description: Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of
Beran p. 40. (Contributed by NM, 7-Aug-2004)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypotheses |
pjoml2.1 |
|- A e. CH |
|
|
pjoml2.2 |
|- B e. CH |
|
|
lecmi.1 |
|- A C_ B |
|
Assertion |
lecmii |
|- A C_H B |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pjoml2.1 |
|- A e. CH |
| 2 |
|
pjoml2.2 |
|- B e. CH |
| 3 |
|
lecmi.1 |
|- A C_ B |
| 4 |
1 2
|
lecmi |
|- ( A C_ B -> A C_H B ) |
| 5 |
3 4
|
ax-mp |
|- A C_H B |