Metamath Proof Explorer


Theorem iccgelbd

Description: An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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