Theorem 3re 9195

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

Syntax hints:   e. wcel 2200  (class class class)co 6007   RRcr 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  11575  ef01bndlem  12283  sin01bnd  12284  cos2bnd  12287  sin01gt0  12289  cos01gt0  12290  egt2lt3  12307  flodddiv4  12463  starvndxnmulrndx  13193  scandxnmulrndx  13205  vscandxnmulrndx  13210  ipndxnmulrndx  13223  tsetndxnmulrndx  13242  plendxnmulrndx  13256  dsndxnmulrndx  13271  slotsdifunifndx  13281  dveflem  15416  sincosq3sgn  15518  sincosq4sgn  15519  cosq23lt0  15523  coseq0q4123  15524  coseq00topi  15525  coseq0negpitopi  15526  tangtx  15528  sincos6thpi  15532  pigt3  15534  pige3  15535  cos02pilt1  15541  lgsdir2lem1  15723  2lgslem3  15796  ex-fl  16172  ex-gcd  16178