Theorem 3re 9216

Description: The number 3 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
3re	⊢ 3 ∈ ℝ

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 9202	. 2 ⊢ 3 = (2 + 1)
2		2re 9212	. . 3 ⊢ 2 ∈ ℝ
3		1re 8177	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8191	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034  2c2 9193  3c3 9194

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8125  ax-addrcl 8128

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9201  df-3 9202

This theorem is referenced by:  3cn  9217  4re  9219  3ne0  9237  3ap0  9238  4pos  9239  1lt3  9314  3lt4  9315  2lt4  9316  3lt5  9319  3lt6  9324  2lt6  9325  3lt7  9330  2lt7  9331  3lt8  9337  2lt8  9338  3lt9  9345  2lt9  9346  1le3  9354  8th4div3  9362  halfpm6th  9363  3halfnz  9576  3lt10  9746  2lt10  9747  5eluz3  9794  uzuzle23  9795  uzuzle34  9797  uz3m2nn  9806  nn01to3  9850  3rp  9893  fz0to4untppr  10358  expnass  10906  sqrt9  11608  ef01bndlem  12316  sin01bnd  12317  cos2bnd  12320  sin01gt0  12322  cos01gt0  12323  egt2lt3  12340  flodddiv4  12496  starvndxnmulrndx  13226  scandxnmulrndx  13238  vscandxnmulrndx  13243  ipndxnmulrndx  13256  tsetndxnmulrndx  13275  plendxnmulrndx  13289  dsndxnmulrndx  13304  slotsdifunifndx  13314  dveflem  15449  sincosq3sgn  15551  sincosq4sgn  15552  cosq23lt0  15556  coseq0q4123  15557  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos6thpi  15565  pigt3  15567  pige3  15568  cos02pilt1  15574  lgsdir2lem1  15756  2lgslem3  15829  ex-fl  16321  ex-gcd  16327