Metamath Proof Explorer

Theorem elioored

Description: A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis elioored.1 
|- ( ph -> A e. ( B (,) C ) )
Assertion elioored 
|- ( ph -> A e. RR )

Proof

Step Hyp Ref Expression
1 elioored.1 
 |-  ( ph -> A e. ( B (,) C ) )
2 elioore 
 |-  ( A e. ( B (,) C ) -> A e. RR )
3 1 2 syl 
 |-  ( ph -> A e. RR )