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 C A 0 A = 0

Proof

Step Hyp Ref Expression
1 chsh A C A S
2 shle0 A S A 0 A = 0
3 1 2 syl A C A 0 A = 0