Theorem 3re 9207

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 9193	. 2 ⊢ 3 = (2 + 1)
2		2re 9203	. . 3 ⊢ 2 ∈ ℝ
3		1re 8168	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8182	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  2c2 9184  3c3 9185

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9192  df-3 9193

This theorem is referenced by:  3cn  9208  4re  9210  3ne0  9228  3ap0  9229  4pos  9230  1lt3  9305  3lt4  9306  2lt4  9307  3lt5  9310  3lt6  9315  2lt6  9316  3lt7  9321  2lt7  9322  3lt8  9328  2lt8  9329  3lt9  9336  2lt9  9337  1le3  9345  8th4div3  9353  halfpm6th  9354  3halfnz  9567  3lt10  9737  2lt10  9738  5eluz3  9785  uzuzle23  9786  uzuzle34  9788  uz3m2nn  9797  nn01to3  9841  3rp  9884  fz0to4untppr  10349  expnass  10897  sqrt9  11599  ef01bndlem  12307  sin01bnd  12308  cos2bnd  12311  sin01gt0  12313  cos01gt0  12314  egt2lt3  12331  flodddiv4  12487  starvndxnmulrndx  13217  scandxnmulrndx  13229  vscandxnmulrndx  13234  ipndxnmulrndx  13247  tsetndxnmulrndx  13266  plendxnmulrndx  13280  dsndxnmulrndx  13295  slotsdifunifndx  13305  dveflem  15440  sincosq3sgn  15542  sincosq4sgn  15543  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos6thpi  15556  pigt3  15558  pige3  15559  cos02pilt1  15565  lgsdir2lem1  15747  2lgslem3  15820  ex-fl  16257  ex-gcd  16263