iccgelb

Description: An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016)

		Ref	Expression
	Assertion	iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in [A, B]) \to A \leq C$

Step	Hyp	Ref	Expression
1		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in [A, B] \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C \leq B))$
2	1	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to (C \in ℝ^{*} \land A \leq C \land C \leq B)$
3	2	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B]) \to A \leq C$
4	3	3impa	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in [A, B]) \to A \leq C$

Metamath Proof Explorer