Theorem 3re 9276

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 9262	. 2 |- 3 = ( 2 + 1 )
2		2re 9272	. . 3 |- 2 e. RR
3		1re 8238	. . 3 |- 1 e. RR
4	2, 3	readdcli 8252	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 3 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095   2c2 9253   3c3 9254

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 2213  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262

This theorem is referenced by:  3cn  9277  4re  9279  3ne0  9297  3ap0  9298  4pos  9299  1lt3  9374  3lt4  9375  2lt4  9376  3lt5  9379  3lt6  9384  2lt6  9385  3lt7  9390  2lt7  9391  3lt8  9397  2lt8  9398  3lt9  9405  2lt9  9406  1le3  9414  8th4div3  9422  halfpm6th  9423  3halfnz  9638  3lt10  9808  2lt10  9809  5eluz3  9856  uzuzle23  9857  uzuzle34  9859  uz3m2nn  9868  nn01to3  9912  3rp  9955  fz0to4untppr  10421  expnass  10970  sqrt9  11688  ef01bndlem  12397  sin01bnd  12398  cos2bnd  12401  sin01gt0  12403  cos01gt0  12404  egt2lt3  12421  flodddiv4  12577  starvndxnmulrndx  13307  scandxnmulrndx  13319  vscandxnmulrndx  13324  ipndxnmulrndx  13337  tsetndxnmulrndx  13356  plendxnmulrndx  13370  dsndxnmulrndx  13385  slotsdifunifndx  13395  dveflem  15537  sincosq3sgn  15639  sincosq4sgn  15640  cosq23lt0  15644  coseq0q4123  15645  coseq00topi  15646  coseq0negpitopi  15647  tangtx  15649  sincos6thpi  15653  pigt3  15655  pige3  15656  cos02pilt1  15662  lgsdir2lem1  15847  2lgslem3  15920  konigsbergiedgwen  16425  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  konigsberglem4  16432  ex-fl  16439  ex-gcd  16445