Theorem 3re 9217

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 9203	. 2 |- 3 = ( 2 + 1 )
2		2re 9213	. . 3 |- 2 e. RR
3		1re 8178	. . 3 |- 1 e. RR
4	2, 3	readdcli 8192	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 3 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035   2c2 9194   3c3 9195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202  df-3 9203

This theorem is referenced by:  3cn  9218  4re  9220  3ne0  9238  3ap0  9239  4pos  9240  1lt3  9315  3lt4  9316  2lt4  9317  3lt5  9320  3lt6  9325  2lt6  9326  3lt7  9331  2lt7  9332  3lt8  9338  2lt8  9339  3lt9  9346  2lt9  9347  1le3  9355  8th4div3  9363  halfpm6th  9364  3halfnz  9577  3lt10  9747  2lt10  9748  5eluz3  9795  uzuzle23  9796  uzuzle34  9798  uz3m2nn  9807  nn01to3  9851  3rp  9894  fz0to4untppr  10359  expnass  10908  sqrt9  11610  ef01bndlem  12319  sin01bnd  12320  cos2bnd  12323  sin01gt0  12325  cos01gt0  12326  egt2lt3  12343  flodddiv4  12499  starvndxnmulrndx  13229  scandxnmulrndx  13241  vscandxnmulrndx  13246  ipndxnmulrndx  13259  tsetndxnmulrndx  13278  plendxnmulrndx  13292  dsndxnmulrndx  13307  slotsdifunifndx  13317  dveflem  15453  sincosq3sgn  15555  sincosq4sgn  15556  cosq23lt0  15560  coseq0q4123  15561  coseq00topi  15562  coseq0negpitopi  15563  tangtx  15565  sincos6thpi  15569  pigt3  15571  pige3  15572  cos02pilt1  15578  lgsdir2lem1  15760  2lgslem3  15833  ex-fl  16338  ex-gcd  16344