Theorem eliccre

Description: A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	eliccre	|- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR )

Proof

Step	Hyp	Ref	Expression
1		elicc2	|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
2	1	biimp3a	|- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> ( C e. RR /\ A <_ C /\ C <_ B ) )
3	2	simp1d	|- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR )