Theorem 3re 9184

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 9170	. 2 |- 3 = ( 2 + 1 )
2		2re 9180	. . 3 |- 2 e. RR
3		1re 8145	. . 3 |- 1 e. RR
4	2, 3	readdcli 8159	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2302	1 |- 3 e. RR

Syntax hints:   e. wcel 2200  (class class class)co 6001   RRcr 7998   1c1 8000   + caddc 8002   2c2 9161   3c3 9162

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 8093  ax-addrcl 8096

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

This theorem is referenced by:  3cn  9185  4re  9187  3ne0  9205  3ap0  9206  4pos  9207  1lt3  9282  3lt4  9283  2lt4  9284  3lt5  9287  3lt6  9292  2lt6  9293  3lt7  9298  2lt7  9299  3lt8  9305  2lt8  9306  3lt9  9313  2lt9  9314  1le3  9322  8th4div3  9330  halfpm6th  9331  3halfnz  9544  3lt10  9714  2lt10  9715  uzuzle23  9766  uz3m2nn  9768  nn01to3  9812  3rp  9855  fz0to4untppr  10320  expnass  10867  sqrt9  11559  ef01bndlem  12267  sin01bnd  12268  cos2bnd  12271  sin01gt0  12273  cos01gt0  12274  egt2lt3  12291  flodddiv4  12447  starvndxnmulrndx  13177  scandxnmulrndx  13189  vscandxnmulrndx  13194  ipndxnmulrndx  13207  tsetndxnmulrndx  13226  plendxnmulrndx  13240  dsndxnmulrndx  13255  slotsdifunifndx  13265  dveflem  15400  sincosq3sgn  15502  sincosq4sgn  15503  cosq23lt0  15507  coseq0q4123  15508  coseq00topi  15509  coseq0negpitopi  15510  tangtx  15512  sincos6thpi  15516  pigt3  15518  pige3  15519  cos02pilt1  15525  lgsdir2lem1  15707  2lgslem3  15780  ex-fl  16089  ex-gcd  16095