Metamath Proof Explorer

Theorem eliccre

Description: A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliccre ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ

Proof

Step Hyp Ref Expression
1 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
2 1 biimp3a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
3 2 simp1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ