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 ( 𝜑𝐴 ∈ ( 𝐵 (,) 𝐶 ) )
Assertion elioored ( 𝜑𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 elioored.1 ( 𝜑𝐴 ∈ ( 𝐵 (,) 𝐶 ) )
2 elioore ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) → 𝐴 ∈ ℝ )
3 1 2 syl ( 𝜑𝐴 ∈ ℝ )