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
|- ( ph -> A e. RR* )
iocleubd.2
|- ( ph -> B e. RR* )
iocleubd.3
|- ( ph -> C e. ( A (,] B ) )
Assertion iocleubd
|- ( ph -> C <_ B )

Proof

Step Hyp Ref Expression
1 iocleubd.1
 |-  ( ph -> A e. RR* )
2 iocleubd.2
 |-  ( ph -> B e. RR* )
3 iocleubd.3
 |-  ( ph -> C e. ( A (,] B ) )
4 iocleub
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> C <_ B )
5 1 2 3 4 syl3anc
 |-  ( ph -> C <_ B )