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 ABCABC

Proof

Step Hyp Ref Expression
1 elicc2 ABCABCACCB
2 1 biimp3a ABCABCACCB
3 2 simp1d ABCABC