Theorem 3re 9112

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 9098	. 2 |- 3 = ( 2 + 1 )
2		2re 9108	. . 3 |- 2 e. RR
3		1re 8073	. . 3 |- 1 e. RR
4	2, 3	readdcli 8087	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2278	1 |- 3 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   2c2 9089   3c3 9090

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9097  df-3 9098

This theorem is referenced by:  3cn  9113  4re  9115  3ne0  9133  3ap0  9134  4pos  9135  1lt3  9210  3lt4  9211  2lt4  9212  3lt5  9215  3lt6  9220  2lt6  9221  3lt7  9226  2lt7  9227  3lt8  9233  2lt8  9234  3lt9  9241  2lt9  9242  1le3  9250  8th4div3  9258  halfpm6th  9259  3halfnz  9472  3lt10  9642  2lt10  9643  uzuzle23  9694  uz3m2nn  9696  nn01to3  9740  3rp  9783  fz0to4untppr  10248  expnass  10792  sqrt9  11392  ef01bndlem  12100  sin01bnd  12101  cos2bnd  12104  sin01gt0  12106  cos01gt0  12107  egt2lt3  12124  flodddiv4  12280  starvndxnmulrndx  13009  scandxnmulrndx  13021  vscandxnmulrndx  13026  ipndxnmulrndx  13039  tsetndxnmulrndx  13058  plendxnmulrndx  13072  dsndxnmulrndx  13087  slotsdifunifndx  13097  dveflem  15231  sincosq3sgn  15333  sincosq4sgn  15334  cosq23lt0  15338  coseq0q4123  15339  coseq00topi  15340  coseq0negpitopi  15341  tangtx  15343  sincos6thpi  15347  pigt3  15349  pige3  15350  cos02pilt1  15356  lgsdir2lem1  15538  2lgslem3  15611  ex-fl  15698  ex-gcd  15704