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	$$⊢\phi \to A\in \left(B,C\right)$$
Assertion	elioored	$$⊢\phi \to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elioored.1	$$⊢\phi \to A\in \left(B,C\right)$$
2		elioore	$$⊢A\in \left(B,C\right)\to A\in ℝ$$
3	1 2	syl	$$⊢\phi \to A\in ℝ$$