Theorem 3re 9083

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 9069	. 2 ⊢ 3 = (2 + 1)
2		2re 9079	. . 3 ⊢ 2 ∈ ℝ
3		1re 8044	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8058	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897  1c1 7899   + caddc 7901  2c2 9060  3c3 9061

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 7992  ax-addrcl 7995

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

This theorem is referenced by:  3cn  9084  4re  9086  3ne0  9104  3ap0  9105  4pos  9106  1lt3  9181  3lt4  9182  2lt4  9183  3lt5  9186  3lt6  9191  2lt6  9192  3lt7  9197  2lt7  9198  3lt8  9204  2lt8  9205  3lt9  9212  2lt9  9213  1le3  9221  8th4div3  9229  halfpm6th  9230  3halfnz  9442  3lt10  9612  2lt10  9613  uzuzle23  9664  uz3m2nn  9666  nn01to3  9710  3rp  9753  fz0to4untppr  10218  expnass  10756  sqrt9  11232  ef01bndlem  11940  sin01bnd  11941  cos2bnd  11944  sin01gt0  11946  cos01gt0  11947  egt2lt3  11964  flodddiv4  12120  starvndxnmulrndx  12848  scandxnmulrndx  12860  vscandxnmulrndx  12865  ipndxnmulrndx  12878  tsetndxnmulrndx  12897  plendxnmulrndx  12911  dsndxnmulrndx  12926  slotsdifunifndx  12936  dveflem  15070  sincosq3sgn  15172  sincosq4sgn  15173  cosq23lt0  15177  coseq0q4123  15178  coseq00topi  15179  coseq0negpitopi  15180  tangtx  15182  sincos6thpi  15186  pigt3  15188  pige3  15189  cos02pilt1  15195  lgsdir2lem1  15377  2lgslem3  15450  ex-fl  15479  ex-gcd  15485