MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3nn Structured version   Visualization version   GIF version

Theorem 3nn 11171
Description: 3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
Assertion
Ref Expression
3nn 3 ∈ ℕ

Proof of Theorem 3nn
StepHypRef Expression
1 df-3 11065 . 2 3 = (2 + 1)
2 2nn 11170 . . 3 2 ∈ ℕ
3 peano2nn 11017 . . 3 (2 ∈ ℕ → (2 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (2 + 1) ∈ ℕ
51, 4eqeltri 2695 1 3 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  (class class class)co 6635  1c1 9922   + caddc 9924  cn 11005  2c2 11055  3c3 11056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-1cn 9979
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-nn 11006  df-2 11064  df-3 11065
This theorem is referenced by:  4nn  11172  3nn0  11295  3z  11395  ige3m2fz  12350  f1oun2prg  13643  sqrlem7  13970  bpoly4  14771  fsumcube  14772  ef01bndlem  14895  sin01bnd  14896  egt2lt3  14915  rpnnen2lem2  14925  rpnnen2lem3  14926  rpnnen2lem4  14927  rpnnen2lem9  14932  rpnnen2lem11  14934  3lcm2e6woprm  15309  3lcm2e6  15421  prmo3  15726  5prm  15796  6nprm  15797  7prm  15798  9nprm  15800  11prm  15803  13prm  15804  17prm  15805  19prm  15806  23prm  15807  prmlem2  15808  37prm  15809  43prm  15810  83prm  15811  139prm  15812  163prm  15813  317prm  15814  631prm  15815  1259lem5  15823  2503lem1  15825  2503lem2  15826  2503lem3  15827  4001lem4  15832  4001prm  15833  mulrndx  15977  mulrid  15978  rngstr  15981  ressmulr  15987  unifndx  16045  unifid  16046  lt6abl  18277  sramulr  19161  opsrmulr  19462  cnfldstr  19729  cnfldfun  19739  zlmmulr  19849  znmul  19871  ressunif  22047  tuslem  22052  tngmulr  22429  vitalilem4  23361  tangtx  24238  1cubrlem  24549  1cubr  24550  dcubic1lem  24551  dcubic2  24552  dcubic  24554  mcubic  24555  cubic2  24556  cubic  24557  quartlem3  24567  quart  24569  log2cnv  24652  log2tlbnd  24653  log2ublem1  24654  log2ublem2  24655  log2ub  24657  ppiublem1  24908  ppiub  24910  chtub  24918  bposlem3  24992  bposlem4  24993  bposlem5  24994  bposlem6  24995  bposlem9  24998  lgsdir2lem5  25035  dchrvmasumlem2  25168  dchrvmasumlema  25170  pntibndlem1  25259  pntibndlem2  25261  pntlema  25266  pntlemb  25267  pntleml  25281  tgcgr4  25407  axlowdimlem16  25818  axlowdimlem17  25819  usgrexmpldifpr  26131  upgr3v3e3cycl  27020  ex-cnv  27264  ex-rn  27267  ex-mod  27276  resvmulr  29809  fib4  30440  circlevma  30694  circlemethhgt  30695  hgt750lema  30709  sinccvglem  31540  cnndvlem1  32503  mblfinlem3  33419  itg2addnclem2  33433  itg2addnclem3  33434  itg2addnc  33435  hlhilsmul  37052  rmydioph  37400  rmxdioph  37402  expdiophlem2  37408  expdioph  37409  amgm3d  38322  lhe4.4ex1a  38348  257prm  41238  fmtno4prmfac193  41250  fmtno4nprmfac193  41251  3ndvds4  41275  139prmALT  41276  31prm  41277  127prm  41280  41prothprm  41301  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem1  41458  tgoldbach  41470  tgoldbachOLD  41477
  Copyright terms: Public domain W3C validator