Theorem 3re 9081

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 9067	. 2 |- 3 = ( 2 + 1 )
2		2re 9077	. . 3 |- 2 e. RR
3		1re 8042	. . 3 |- 1 e. RR
4	2, 3	readdcli 8056	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 3 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899   2c2 9058   3c3 9059

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9066  df-3 9067

This theorem is referenced by:  3cn  9082  4re  9084  3ne0  9102  3ap0  9103  4pos  9104  1lt3  9179  3lt4  9180  2lt4  9181  3lt5  9184  3lt6  9189  2lt6  9190  3lt7  9195  2lt7  9196  3lt8  9202  2lt8  9203  3lt9  9210  2lt9  9211  1le3  9219  8th4div3  9227  halfpm6th  9228  3halfnz  9440  3lt10  9610  2lt10  9611  uzuzle23  9662  uz3m2nn  9664  nn01to3  9708  3rp  9751  fz0to4untppr  10216  expnass  10754  sqrt9  11230  ef01bndlem  11938  sin01bnd  11939  cos2bnd  11942  sin01gt0  11944  cos01gt0  11945  egt2lt3  11962  flodddiv4  12118  starvndxnmulrndx  12846  scandxnmulrndx  12858  vscandxnmulrndx  12863  ipndxnmulrndx  12876  tsetndxnmulrndx  12895  plendxnmulrndx  12909  dsndxnmulrndx  12924  slotsdifunifndx  12934  dveflem  15046  sincosq3sgn  15148  sincosq4sgn  15149  cosq23lt0  15153  coseq0q4123  15154  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  sincos6thpi  15162  pigt3  15164  pige3  15165  cos02pilt1  15171  lgsdir2lem1  15353  2lgslem3  15426  ex-fl  15455  ex-gcd  15461