This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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