Theorem 3re 9109

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 9095	. 2 ⊢ 3 = (2 + 1)
2		2re 9105	. . 3 ⊢ 2 ∈ ℝ
3		1re 8070	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8084	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2277	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  2c2 9086  3c3 9087

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094  df-3 9095

This theorem is referenced by:  3cn  9110  4re  9112  3ne0  9130  3ap0  9131  4pos  9132  1lt3  9207  3lt4  9208  2lt4  9209  3lt5  9212  3lt6  9217  2lt6  9218  3lt7  9223  2lt7  9224  3lt8  9230  2lt8  9231  3lt9  9238  2lt9  9239  1le3  9247  8th4div3  9255  halfpm6th  9256  3halfnz  9469  3lt10  9639  2lt10  9640  uzuzle23  9691  uz3m2nn  9693  nn01to3  9737  3rp  9780  fz0to4untppr  10245  expnass  10788  sqrt9  11330  ef01bndlem  12038  sin01bnd  12039  cos2bnd  12042  sin01gt0  12044  cos01gt0  12045  egt2lt3  12062  flodddiv4  12218  starvndxnmulrndx  12947  scandxnmulrndx  12959  vscandxnmulrndx  12964  ipndxnmulrndx  12977  tsetndxnmulrndx  12996  plendxnmulrndx  13010  dsndxnmulrndx  13025  slotsdifunifndx  13035  dveflem  15169  sincosq3sgn  15271  sincosq4sgn  15272  cosq23lt0  15276  coseq0q4123  15277  coseq00topi  15278  coseq0negpitopi  15279  tangtx  15281  sincos6thpi  15285  pigt3  15287  pige3  15288  cos02pilt1  15294  lgsdir2lem1  15476  2lgslem3  15549  ex-fl  15623  ex-gcd  15629