Theorem 3re 9056

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 9042	. 2 ⊢ 3 = (2 + 1)
2		2re 9052	. . 3 ⊢ 2 ∈ ℝ
3		1re 8018	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8032	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2266	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5918  ℝcr 7871  1c1 7873   + caddc 7875  2c2 9033  3c3 9034

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9041  df-3 9042

This theorem is referenced by:  3cn  9057  4re  9059  3ne0  9077  3ap0  9078  4pos  9079  1lt3  9153  3lt4  9154  2lt4  9155  3lt5  9158  3lt6  9163  2lt6  9164  3lt7  9169  2lt7  9170  3lt8  9176  2lt8  9177  3lt9  9184  2lt9  9185  1le3  9193  8th4div3  9201  halfpm6th  9202  3halfnz  9414  3lt10  9584  2lt10  9585  uzuzle23  9636  uz3m2nn  9638  nn01to3  9682  3rp  9725  fz0to4untppr  10190  expnass  10716  sqrt9  11192  ef01bndlem  11899  sin01bnd  11900  cos2bnd  11903  sin01gt0  11905  cos01gt0  11906  egt2lt3  11923  flodddiv4  12075  starvndxnmulrndx  12761  scandxnmulrndx  12773  vscandxnmulrndx  12778  ipndxnmulrndx  12791  tsetndxnmulrndx  12810  plendxnmulrndx  12824  dsndxnmulrndx  12835  slotsdifunifndx  12845  dveflem  14872  sincosq3sgn  14963  sincosq4sgn  14964  cosq23lt0  14968  coseq0q4123  14969  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos6thpi  14977  pigt3  14979  pige3  14980  cos02pilt1  14986  lgsdir2lem1  15144  ex-fl  15217  ex-gcd  15223