Theorem 3re 8113

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

Assertion

Ref	Expression
3re	|- 3 e. RR

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 8099	. 2 |- 3 = ( 2 + 1 )
2		2re 8109	. . 3 |- 2 e. RR
3		1re 7118	. . 3 |- 1 e. RR
4	2, 3	readdcli 7132	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2151	1 |- 3 e. RR

Syntax hints:   e. wcel 1433  (class class class)co 5532   RRcr 6980   1c1 6982   + caddc 6984   2c2 8089   3c3 8090

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077  df-2 8098  df-3 8099

This theorem is referenced by:  3cn  8114  4re  8116  3ne0  8134  3ap0  8135  4pos  8136  1lt3  8203  3lt4  8204  2lt4  8205  3lt5  8208  3lt6  8213  2lt6  8214  3lt7  8219  2lt7  8220  3lt8  8226  2lt8  8227  3lt9  8234  2lt9  8235  1le3  8242  8th4div3  8250  halfpm6th  8251  3halfnz  8444  3lt10  8613  2lt10  8614  uzuzle23  8659  uz3m2nn  8661  nn01to3  8702  expnass  9580  sqrt9  9934  flodddiv4  10334  ex-fl  10563  ex-gcd  10568