Theorem 3re 9328

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 9314	. 2 |- 3 = ( 2 + 1 )
2		2re 9324	. . 3 |- 2 e. RR
3		1re 8289	. . 3 |- 1 e. RR
4	2, 3	readdcli 8303	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2307	1 |- 3 e. RR

Syntax hints:   e. wcel 2205  (class class class)co 6058   RRcr 8142   1c1 8144   + caddc 8146   2c2 9305   3c3 9306

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 2216  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-2 9313  df-3 9314

This theorem is referenced by:  3cn  9329  4re  9331  3ne0  9349  3ap0  9350  4pos  9351  1lt3  9426  3lt4  9427  2lt4  9428  3lt5  9431  3lt6  9436  2lt6  9437  3lt7  9442  2lt7  9443  3lt8  9449  2lt8  9450  3lt9  9457  2lt9  9458  1le3  9466  8th4div3  9474  halfpm6th  9475  3halfnz  9693  3lt10  9863  2lt10  9864  5eluz3  9911  uzuzle23  9912  uzuzle34  9914  uz3m2nn  9923  nn01to3  9967  3rp  10010  fz0to4untppr  10480  expnass  11031  sqrt9  11758  ef01bndlem  12467  sin01bnd  12468  cos2bnd  12471  sin01gt0  12473  cos01gt0  12474  egt2lt3  12491  flodddiv4  12647  starvndxnmulrndx  13441  scandxnmulrndx  13453  vscandxnmulrndx  13458  ipndxnmulrndx  13471  tsetndxnmulrndx  13490  plendxnmulrndx  13504  dsndxnmulrndx  13519  slotsdifunifndx  13529  dveflem  15717  sincosq3sgn  15819  sincosq4sgn  15820  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos6thpi  15833  pigt3  15835  pige3  15836  cos02pilt1  15842  lgsdir2lem1  16027  2lgslem3  16100  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem4  16612  ex-fl  16619  ex-gcd  16625