Metamath Proof Explorer


Theorem iocleub

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

Ref Expression
Assertion iocleub A * B * C A B C B

Proof

Step Hyp Ref Expression
1 elioc1 A * B * C A B C * A < C C B
2 simp3 C * A < C C B C B
3 1 2 syl6bi A * B * C A B C B
4 3 3impia A * B * C A B C B