Theorem 3re 9311

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

Assertion

Ref	Expression
3re	⊢ 3 ∈ ℝ

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 9297	. 2 ⊢ 3 = (2 + 1)
2		2re 9307	. . 3 ⊢ 2 ∈ ℝ
3		1re 8273	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8287	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2305	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126  1c1 8128   + caddc 8130  2c2 9288  3c3 9289

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297

This theorem is referenced by:  3cn  9312  4re  9314  3ne0  9332  3ap0  9333  4pos  9334  1lt3  9409  3lt4  9410  2lt4  9411  3lt5  9414  3lt6  9419  2lt6  9420  3lt7  9425  2lt7  9426  3lt8  9432  2lt8  9433  3lt9  9440  2lt9  9441  1le3  9449  8th4div3  9457  halfpm6th  9458  3halfnz  9675  3lt10  9845  2lt10  9846  5eluz3  9893  uzuzle23  9894  uzuzle34  9896  uz3m2nn  9905  nn01to3  9949  3rp  9992  fz0to4untppr  10458  expnass  11007  sqrt9  11733  ef01bndlem  12442  sin01bnd  12443  cos2bnd  12446  sin01gt0  12448  cos01gt0  12449  egt2lt3  12466  flodddiv4  12622  starvndxnmulrndx  13357  scandxnmulrndx  13369  vscandxnmulrndx  13374  ipndxnmulrndx  13387  tsetndxnmulrndx  13406  plendxnmulrndx  13420  dsndxnmulrndx  13435  slotsdifunifndx  13445  dveflem  15591  sincosq3sgn  15693  sincosq4sgn  15694  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos6thpi  15707  pigt3  15709  pige3  15710  cos02pilt1  15716  lgsdir2lem1  15901  2lgslem3  15974  konigsbergiedgwen  16479  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem4  16486  ex-fl  16493  ex-gcd  16499