Metamath Proof Explorer


Theorem zrei

Description: An integer is a real number. (Contributed by NM, 14-Jul-2005)

Ref Expression
Hypothesis zrei.1 A
Assertion zrei A

Proof

Step Hyp Ref Expression
1 zrei.1 A
2 zre A A
3 1 2 ax-mp A