Metamath Proof Explorer


Theorem qred

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

Ref Expression
Hypothesis qred.1 φA
Assertion qred φA

Proof

Step Hyp Ref Expression
1 qred.1 φA
2 qre AA
3 1 2 syl φA