Metamath Proof Explorer


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 )