Theorem 3re 8996

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 8982	. 2 ⊢ 3 = (2 + 1)
2		2re 8992	. . 3 ⊢ 2 ∈ ℝ
3		1re 7959	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7973	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5878  ℝcr 7813  1c1 7815   + caddc 7817  2c2 8973  3c3 8974

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8981  df-3 8982

This theorem is referenced by:  3cn  8997  4re  8999  3ne0  9017  3ap0  9018  4pos  9019  1lt3  9093  3lt4  9094  2lt4  9095  3lt5  9098  3lt6  9103  2lt6  9104  3lt7  9109  2lt7  9110  3lt8  9116  2lt8  9117  3lt9  9124  2lt9  9125  1le3  9133  8th4div3  9141  halfpm6th  9142  3halfnz  9353  3lt10  9523  2lt10  9524  uzuzle23  9574  uz3m2nn  9576  nn01to3  9620  3rp  9662  fz0to4untppr  10127  expnass  10629  sqrt9  11060  ef01bndlem  11767  sin01bnd  11768  cos2bnd  11771  sin01gt0  11772  cos01gt0  11773  egt2lt3  11790  flodddiv4  11942  starvndxnmulrndx  12605  scandxnmulrndx  12617  vscandxnmulrndx  12622  ipndxnmulrndx  12635  tsetndxnmulrndx  12654  plendxnmulrndx  12668  dsndxnmulrndx  12679  slotsdifunifndx  12689  dveflem  14348  sincosq3sgn  14410  sincosq4sgn  14411  cosq23lt0  14415  coseq0q4123  14416  coseq00topi  14417  coseq0negpitopi  14418  tangtx  14420  sincos6thpi  14424  pigt3  14426  pige3  14427  cos02pilt1  14433  lgsdir2lem1  14590  ex-fl  14638  ex-gcd  14644