Theorem eliccd

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

	Ref	Expression
Hypotheses	eliccd.1	$$⊢\phi \to A\in ℝ$$
	eliccd.2	$$⊢\phi \to B\in ℝ$$
	eliccd.3	$$⊢\phi \to C\in ℝ$$
	eliccd.4	$$⊢\phi \to A\le C$$
	eliccd.5	$$⊢\phi \to C\le B$$
Assertion	eliccd	$$⊢\phi \to C\in \left[A,B\right]$$

Proof

Step	Hyp	Ref	Expression
1		eliccd.1	$$⊢\phi \to A\in ℝ$$
2		eliccd.2	$$⊢\phi \to B\in ℝ$$
3		eliccd.3	$$⊢\phi \to C\in ℝ$$
4		eliccd.4	$$⊢\phi \to A\le C$$
5		eliccd.5	$$⊢\phi \to C\le B$$
6		elicc2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(C\in \left[A,B\right]\leftrightarrow \left(C\in ℝ\wedge A\le C\wedge C\le B\right)\right)$$
7	1 2 6	syl2anc	$$⊢\phi \to \left(C\in \left[A,B\right]\leftrightarrow \left(C\in ℝ\wedge A\le C\wedge C\le B\right)\right)$$
8	3 4 5 7	mpbir3and	$$⊢\phi \to C\in \left[A,B\right]$$