Theorem 3re 9217

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 9203	. 2 ⊢ 3 = (2 + 1)
2		2re 9213	. . 3 ⊢ 2 ∈ ℝ
3		1re 8178	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8192	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031  1c1 8033   + caddc 8035  2c2 9194  3c3 9195

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 8126  ax-addrcl 8129

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

This theorem is referenced by:  3cn  9218  4re  9220  3ne0  9238  3ap0  9239  4pos  9240  1lt3  9315  3lt4  9316  2lt4  9317  3lt5  9320  3lt6  9325  2lt6  9326  3lt7  9331  2lt7  9332  3lt8  9338  2lt8  9339  3lt9  9346  2lt9  9347  1le3  9355  8th4div3  9363  halfpm6th  9364  3halfnz  9577  3lt10  9747  2lt10  9748  5eluz3  9795  uzuzle23  9796  uzuzle34  9798  uz3m2nn  9807  nn01to3  9851  3rp  9894  fz0to4untppr  10359  expnass  10908  sqrt9  11626  ef01bndlem  12335  sin01bnd  12336  cos2bnd  12339  sin01gt0  12341  cos01gt0  12342  egt2lt3  12359  flodddiv4  12515  starvndxnmulrndx  13245  scandxnmulrndx  13257  vscandxnmulrndx  13262  ipndxnmulrndx  13275  tsetndxnmulrndx  13294  plendxnmulrndx  13308  dsndxnmulrndx  13323  slotsdifunifndx  13333  dveflem  15469  sincosq3sgn  15571  sincosq4sgn  15572  cosq23lt0  15576  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos6thpi  15585  pigt3  15587  pige3  15588  cos02pilt1  15594  lgsdir2lem1  15776  2lgslem3  15849  konigsbergiedgwen  16354  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem4  16361  ex-fl  16368  ex-gcd  16374