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

Metamath Proof Explorer

Theorem eliccxrd

Description: Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses eliccxrd.1 ⊢ φ → A ∈ ℝ *
eliccxrd.2 ⊢ φ → B ∈ ℝ *
eliccxrd.3 ⊢ φ → C ∈ ℝ *
eliccxrd.4 ⊢ φ → A ≤ C
eliccxrd.5 ⊢ φ → C ≤ B
Assertion eliccxrd ⊢ φ → C ∈ A B

Proof

Step Hyp Ref Expression
1 eliccxrd.1 ⊢ φ → A ∈ ℝ *
2 eliccxrd.2 ⊢ φ → B ∈ ℝ *
3 eliccxrd.3 ⊢ φ → C ∈ ℝ *
4 eliccxrd.4 ⊢ φ → A ≤ C
5 eliccxrd.5 ⊢ φ → C ≤ B
6 4 5 jca ⊢ φ → A ≤ C ∧ C ≤ B
7 elicc4 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B
8 1 2 3 7 syl3anc ⊢ φ → C ∈ A B ↔ A ≤ C ∧ C ≤ B
9 6 8 mpbird ⊢ φ → C ∈ A B