Metamath Proof Explorer

Theorem chle0

Description: No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chle0 
|- ( A e. CH -> ( A C_ 0H <-> A = 0H ) )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( A e. CH -> A e. SH )
2 shle0 
 |-  ( A e. SH -> ( A C_ 0H <-> A = 0H ) )
3 1 2 syl 
 |-  ( A e. CH -> ( A C_ 0H <-> A = 0H ) )