Theorem qred

Description: A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	qred.1	$$⊢\phi \to A\in \mathbb{Q}$$
Assertion	qred	$$⊢\phi \to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		qred.1	$$⊢\phi \to A\in \mathbb{Q}$$
2		qre	$$⊢A\in \mathbb{Q}\to A\in ℝ$$
3	1 2	syl	$$⊢\phi \to A\in ℝ$$