Metamath Proof Explorer


Theorem icoltubd

Description: An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 icoltubd.1 φ A *
2 icoltubd.2 φ B *
3 icoltubd.3 φ C A B
4 icoltub A * B * C A B C < B
5 1 2 3 4 syl3anc φ C < B