Theorem 3re 9195

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 9181	. 2 ⊢ 3 = (2 + 1)
2		2re 9191	. . 3 ⊢ 2 ∈ ℝ
3		1re 8156	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8170	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009  1c1 8011   + caddc 8013  2c2 9172  3c3 9173

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 8104  ax-addrcl 8107

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

This theorem is referenced by:  3cn  9196  4re  9198  3ne0  9216  3ap0  9217  4pos  9218  1lt3  9293  3lt4  9294  2lt4  9295  3lt5  9298  3lt6  9303  2lt6  9304  3lt7  9309  2lt7  9310  3lt8  9316  2lt8  9317  3lt9  9324  2lt9  9325  1le3  9333  8th4div3  9341  halfpm6th  9342  3halfnz  9555  3lt10  9725  2lt10  9726  uzuzle23  9778  uz3m2nn  9780  nn01to3  9824  3rp  9867  fz0to4untppr  10332  expnass  10879  sqrt9  11574  ef01bndlem  12282  sin01bnd  12283  cos2bnd  12286  sin01gt0  12288  cos01gt0  12289  egt2lt3  12306  flodddiv4  12462  starvndxnmulrndx  13192  scandxnmulrndx  13204  vscandxnmulrndx  13209  ipndxnmulrndx  13222  tsetndxnmulrndx  13241  plendxnmulrndx  13255  dsndxnmulrndx  13270  slotsdifunifndx  13280  dveflem  15415  sincosq3sgn  15517  sincosq4sgn  15518  cosq23lt0  15522  coseq0q4123  15523  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  sincos6thpi  15531  pigt3  15533  pige3  15534  cos02pilt1  15540  lgsdir2lem1  15722  2lgslem3  15795  ex-fl  16144  ex-gcd  16150