Metamath Proof Explorer


Theorem 3re

Description: The number 3 is real. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion 3re 3

Proof

Step Hyp Ref Expression
1 df-3 3=2+1
2 2re 2
3 1re 1
4 2 3 readdcli 2+1
5 1 4 eqeltri 3