Theorem 3re 8927

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 8913	. 2 |- 3 = ( 2 + 1 )
2		2re 8923	. . 3 |- 2 e. RR
3		1re 7894	. . 3 |- 1 e. RR
4	2, 3	readdcli 7908	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2238	1 |- 3 e. RR

Syntax hints:   e. wcel 2136  (class class class)co 5841   RRcr 7748   1c1 7750   + caddc 7752   2c2 8904   3c3 8905

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8912  df-3 8913

This theorem is referenced by:  3cn  8928  4re  8930  3ne0  8948  3ap0  8949  4pos  8950  1lt3  9024  3lt4  9025  2lt4  9026  3lt5  9029  3lt6  9034  2lt6  9035  3lt7  9040  2lt7  9041  3lt8  9047  2lt8  9048  3lt9  9055  2lt9  9056  1le3  9064  8th4div3  9072  halfpm6th  9073  3halfnz  9284  3lt10  9454  2lt10  9455  uzuzle23  9505  uz3m2nn  9507  nn01to3  9551  3rp  9591  fz0to4untppr  10055  expnass  10556  sqrt9  10986  ef01bndlem  11693  sin01bnd  11694  cos2bnd  11697  sin01gt0  11698  cos01gt0  11699  egt2lt3  11716  flodddiv4  11867  dveflem  13287  sincosq3sgn  13349  sincosq4sgn  13350  cosq23lt0  13354  coseq0q4123  13355  coseq00topi  13356  coseq0negpitopi  13357  tangtx  13359  sincos6thpi  13363  pigt3  13365  pige3  13366  cos02pilt1  13372  lgsdir2lem1  13529  ex-fl  13566  ex-gcd  13572