Metamath Proof Explorer


Theorem re1

Description: The real part of one. (Contributed by Scott Fenton, 9-Jun-2006)

Ref Expression
Assertion re1 1=1

Proof

Step Hyp Ref Expression
1 1re 1
2 rere 11=1
3 1 2 ax-mp 1=1