Metamath Proof Explorer


Theorem iocleubd

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

Ref Expression
Hypotheses iocleubd.1 φ A *
iocleubd.2 φ B *
iocleubd.3 φ C A B
Assertion iocleubd φ C B

Proof

Step Hyp Ref Expression
1 iocleubd.1 φ A *
2 iocleubd.2 φ B *
3 iocleubd.3 φ C A B
4 iocleub A * B * C A B C B
5 1 2 3 4 syl3anc φ C B