Theorem 3re 9180

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 9166	. 2 ⊢ 3 = (2 + 1)
2		2re 9176	. . 3 ⊢ 2 ∈ ℝ
3		1re 8141	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8155	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994  1c1 7996   + caddc 7998  2c2 9157  3c3 9158

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9165  df-3 9166

This theorem is referenced by:  3cn  9181  4re  9183  3ne0  9201  3ap0  9202  4pos  9203  1lt3  9278  3lt4  9279  2lt4  9280  3lt5  9283  3lt6  9288  2lt6  9289  3lt7  9294  2lt7  9295  3lt8  9301  2lt8  9302  3lt9  9309  2lt9  9310  1le3  9318  8th4div3  9326  halfpm6th  9327  3halfnz  9540  3lt10  9710  2lt10  9711  uzuzle23  9762  uz3m2nn  9764  nn01to3  9808  3rp  9851  fz0to4untppr  10316  expnass  10862  sqrt9  11554  ef01bndlem  12262  sin01bnd  12263  cos2bnd  12266  sin01gt0  12268  cos01gt0  12269  egt2lt3  12286  flodddiv4  12442  starvndxnmulrndx  13172  scandxnmulrndx  13184  vscandxnmulrndx  13189  ipndxnmulrndx  13202  tsetndxnmulrndx  13221  plendxnmulrndx  13235  dsndxnmulrndx  13250  slotsdifunifndx  13260  dveflem  15394  sincosq3sgn  15496  sincosq4sgn  15497  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  sincos6thpi  15510  pigt3  15512  pige3  15513  cos02pilt1  15519  lgsdir2lem1  15701  2lgslem3  15774  ex-fl  16047  ex-gcd  16053