Metamath Proof Explorer

Theorem icogelb

Description: An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion icogelb A * B * C A B A C


Step Hyp Ref Expression
1 elico1 A * B * C A B C * A C C < B
2 simp2 C * A C C < B A C
3 1 2 syl6bi A * B * C A B A C
4 3 3impia A * B * C A B A C