Metamath Proof Explorer

Theorem elicc4

Description: Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014) (Proof shortened by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion elicc4 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B

Proof

Step Hyp Ref Expression
1 elicc1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A ≤ C ∧ C ≤ B
2 3anass ⊢ C ∈ ℝ * ∧ A ≤ C ∧ C ≤ B ↔ C ∈ ℝ * ∧ A ≤ C ∧ C ≤ B
3 1 2 bitrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A ≤ C ∧ C ≤ B
4 3 baibd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B
5 4 3impa ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B