Theorem 3re 9058

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 9044	. 2 |- 3 = ( 2 + 1 )
2		2re 9054	. . 3 |- 2 e. RR
3		1re 8020	. . 3 |- 1 e. RR
4	2, 3	readdcli 8034	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2266	1 |- 3 e. RR

Syntax hints:   e. wcel 2164  (class class class)co 5919   RRcr 7873   1c1 7875   + caddc 7877   2c2 9035   3c3 9036

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9043  df-3 9044

This theorem is referenced by:  3cn  9059  4re  9061  3ne0  9079  3ap0  9080  4pos  9081  1lt3  9156  3lt4  9157  2lt4  9158  3lt5  9161  3lt6  9166  2lt6  9167  3lt7  9172  2lt7  9173  3lt8  9179  2lt8  9180  3lt9  9187  2lt9  9188  1le3  9196  8th4div3  9204  halfpm6th  9205  3halfnz  9417  3lt10  9587  2lt10  9588  uzuzle23  9639  uz3m2nn  9641  nn01to3  9685  3rp  9728  fz0to4untppr  10193  expnass  10719  sqrt9  11195  ef01bndlem  11902  sin01bnd  11903  cos2bnd  11906  sin01gt0  11908  cos01gt0  11909  egt2lt3  11926  flodddiv4  12078  starvndxnmulrndx  12764  scandxnmulrndx  12776  vscandxnmulrndx  12781  ipndxnmulrndx  12794  tsetndxnmulrndx  12813  plendxnmulrndx  12827  dsndxnmulrndx  12838  slotsdifunifndx  12848  dveflem  14905  sincosq3sgn  15004  sincosq4sgn  15005  cosq23lt0  15009  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos6thpi  15018  pigt3  15020  pige3  15021  cos02pilt1  15027  lgsdir2lem1  15185  2lgslem3  15258  ex-fl  15287  ex-gcd  15293