Theorem 3nn 12098

Description: 3 is a positive integer. (Contributed by NM, 8-Jan-2006.)

Assertion

Ref	Expression
3nn	⊢ 3 ∈ ℕ

Proof of Theorem 3nn

Step	Hyp	Ref	Expression
1		df-3 12083	. 2 ⊢ 3 = (2 + 1)
2		2nn 12092	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12031	. . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (2 + 1) ∈ ℕ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℕ

Syntax hints:   ∈ wcel 2104  (class class class)co 7307  1c1 10918   + caddc 10920  ℕcn 12019  2c2 12074  3c3 12075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-2 12082  df-3 12083

This theorem is referenced by:  4nn  12102  3nn0  12297  3z  12399  ige3m2fz  13326  f1oun2prg  14675  sqrlem7  15005  bpoly4  15814  fsumcube  15815  sin01bnd  15939  egt2lt3  15960  rpnnen2lem2  15969  rpnnen2lem3  15970  rpnnen2lem4  15971  rpnnen2lem9  15976  rpnnen2lem11  15978  3lcm2e6woprm  16365  3lcm2e6  16481  prmo3  16787  5prm  16855  6nprm  16856  7prm  16857  9nprm  16859  11prm  16861  13prm  16862  17prm  16863  19prm  16864  23prm  16865  prmlem2  16866  37prm  16867  43prm  16868  83prm  16869  139prm  16870  163prm  16871  317prm  16872  631prm  16873  1259lem5  16881  2503lem1  16883  2503lem2  16884  2503lem3  16885  4001lem4  16890  4001prm  16891  mulrndx  17048  mulrid  17049  rngstr  17053  unifndx  17150  unifid  17151  unifndxnn  17152  slotsdifunifndx  17156  lt6abl  19541  sramulrOLD  20491  cnfldstr  20644  cnfldfunALTOLD  20656  zlmmulrOLD  20770  znmulOLD  20794  opsrmulrOLD  21302  tuslemOLD  23464  tngmulrOLD  23849  tangtx  25707  1cubrlem  26036  1cubr  26037  dcubic1lem  26038  dcubic2  26039  dcubic  26041  mcubic  26042  cubic2  26043  cubic  26044  quartlem3  26054  quart  26056  log2cnv  26139  log2tlbnd  26140  log2ublem1  26141  log2ublem2  26142  log2ub  26144  ppiublem1  26395  ppiub  26397  chtub  26405  bposlem3  26479  bposlem4  26480  bposlem5  26481  bposlem6  26482  bposlem9  26485  lgsdir2lem5  26522  dchrvmasumlem2  26691  dchrvmasumlema  26693  pntleml  26804  tgcgr4  26937  axlowdimlem16  27370  axlowdimlem17  27371  usgrexmpldifpr  27670  upgr3v3e3cycl  28589  ex-cnv  28846  ex-rn  28849  ex-mod  28858  resvmulrOLD  31584  fib4  32416  circlevma  32667  circlemethhgt  32668  hgt750lema  32682  sinccvglem  33675  cnndvlem1  34762  mblfinlem3  35860  itg2addnclem2  35873  itg2addnc  35875  hlhilsmulOLD  40001  lcm3un  40065  aks4d1p1  40126  3cubeslem2  40544  3cubeslem3r  40546  3cubes  40549  rmydioph  40874  rmxdioph  40876  expdiophlem2  40882  expdioph  40883  amgm3d  41848  lhe4.4ex1a  41985  257prm  45071  fmtno4prmfac193  45083  fmtno4nprmfac193  45084  3ndvds4  45105  139prmALT  45106  31prm  45107  127prm  45109  41prothprm  45129  341fppr2  45244  nfermltl2rev  45253  wtgoldbnnsum4prm  45312  bgoldbnnsum3prm  45314  bgoldbtbndlem1  45315  tgoldbach  45327