Metamath Proof Explorer

Theorem 3re

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

Ref Expression
Assertion 3re 
|- 3 e. RR

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 2re 
 |-  2 e. RR
3 1re 
 |-  1 e. RR
4 2 3 readdcli 
 |-  ( 2 + 1 ) e. RR
5 1 4 eqeltri 
 |-  3 e. RR