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∈AB↔A≤C∧C≤B

Proof

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