Theorem 3re 8952

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 8938	. 2 |- 3 = ( 2 + 1 )
2		2re 8948	. . 3 |- 2 e. RR
3		1re 7919	. . 3 |- 1 e. RR
4	2, 3	readdcli 7933	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2243	1 |- 3 e. RR

Syntax hints:   e. wcel 2141  (class class class)co 5853   RRcr 7773   1c1 7775   + caddc 7777   2c2 8929   3c3 8930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-2 8937  df-3 8938

This theorem is referenced by:  3cn  8953  4re  8955  3ne0  8973  3ap0  8974  4pos  8975  1lt3  9049  3lt4  9050  2lt4  9051  3lt5  9054  3lt6  9059  2lt6  9060  3lt7  9065  2lt7  9066  3lt8  9072  2lt8  9073  3lt9  9080  2lt9  9081  1le3  9089  8th4div3  9097  halfpm6th  9098  3halfnz  9309  3lt10  9479  2lt10  9480  uzuzle23  9530  uz3m2nn  9532  nn01to3  9576  3rp  9616  fz0to4untppr  10080  expnass  10581  sqrt9  11012  ef01bndlem  11719  sin01bnd  11720  cos2bnd  11723  sin01gt0  11724  cos01gt0  11725  egt2lt3  11742  flodddiv4  11893  dveflem  13481  sincosq3sgn  13543  sincosq4sgn  13544  cosq23lt0  13548  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos6thpi  13557  pigt3  13559  pige3  13560  cos02pilt1  13566  lgsdir2lem1  13723  ex-fl  13760  ex-gcd  13766