Metamath Proof Explorer

Theorem elicc2i

Description: Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Hypotheses elicc2i.1 ⊢ A ∈ ℝ
elicc2i.2 ⊢ B ∈ ℝ
Assertion elicc2i ⊢ C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B

Proof

Step Hyp Ref Expression
1 elicc2i.1 ⊢ A ∈ ℝ
2 elicc2i.2 ⊢ B ∈ ℝ
3 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B
4 1 2 3 mp2an ⊢ C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B