MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3re Unicode version

Theorem 3re 10634
Description: The number 3 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
3re

Proof of Theorem 3re
StepHypRef Expression
1 df-3 10620 . 2
2 2re 10630 . . 3
3 1re 9616 . . 3
42, 3readdcli 9630 . 2
51, 4eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cr 9512  1c1 9514   caddc 9516  2c2 10610  3c3 10611
This theorem is referenced by:  3cn  10635  4re  10637  3ne0  10655  4pos  10656  1lt3  10729  3lt4  10730  2lt4  10731  3lt5  10734  3lt6  10739  2lt6  10740  3lt7  10745  2lt7  10746  3lt8  10752  2lt8  10753  3lt9  10760  2lt9  10761  3lt10  10769  2lt10  10770  1le3  10777  uzuzle23  11150  uz3m2nn  11152  nn01to3  11204  expnass  12273  hashtpg  12523  sqrlem7  13082  sqrt9  13107  caucvgrlem  13495  caurcvgr  13496  ef01bndlem  13919  sin01bnd  13920  cos2bnd  13923  sin01gt0  13925  cos01gt0  13926  egt2lt3  13939  rpnnen2lem3  13950  rpnnen2lem4  13951  rpnnen2lem9  13956  matsca  18917  matvsca  18918  vitalilem4  22020  dveflem  22380  sincosq3sgn  22893  sincosq4sgn  22894  tangtx  22898  sincos6thpi  22908  pige3  22910  ang180lem2  23142  1cubrlem  23172  log2cnv  23275  log2tlbnd  23276  log2ub  23280  cxploglim2  23308  basellem5  23358  basellem9  23362  cht3  23447  ppiublem1  23477  ppiub  23479  chtub  23487  bposlem2  23560  bposlem3  23561  bposlem4  23562  bposlem5  23563  bposlem6  23564  bposlem8  23566  bposlem9  23567  lgsdir2lem1  23598  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  chto1ub  23661  dchrvmasumlem2  23683  dchrvmasumlema  23685  dchrvmasumiflem1  23686  mulog2sumlem2  23720  pntibndlem1  23774  pntibndlem2  23776  pntlemb  23782  pntlemk  23791  pntlemo  23792  axlowdimlem8  24252  axlowdimlem9  24253  axlowdimlem16  24260  axlowdimlem17  24261  axlowdim  24264  usgraexvlem  24395  usgraex3elv  24399  constr3pthlem3  24657  4cycl4v4e  24666  4cycl4dv4e  24668  konigsberg  24987  extwwlkfablem2  25078  numclwlk1lem2f1  25094  frgraogt3nreg  25120  friendshipgt3  25121  friendship  25122  ex-dif  25144  ex-in  25146  ex-1st  25165  ex-2nd  25166  ex-fl  25168  stadd3i  27167  resvmulr  27825  problem3  29021  problem5  29023  bpoly4  29821  itg2addnclem2  30067  heiborlem5  30311  heiborlem6  30312  heiborlem7  30313  heiborlem8  30314  jm2.23  30938  jm2.20nn  30939  3rp  31471  lt4addmuld  31506  stoweidlem11  31793  stoweidlem13  31795  stoweidlem26  31808  stoweidlem34  31816  stoweidlem42  31824  stoweidlem59  31841  stoweidlem62  31844  stoweid  31845  wallispilem4  31850  fourierdlem87  31976  pgrpgt2nabl  32959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619  df-3 10620
  Copyright terms: Public domain W3C validator