Theorem 3nn 12199

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 12184	. 2 ⊢ 3 = (2 + 1)
2		2nn 12193	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12132	. . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (2 + 1) ∈ ℕ
5	1, 4	eqeltri 2827	1 ⊢ 3 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7341  1c1 11002   + caddc 11004  ℕcn 12120  2c2 12175  3c3 12176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-1cn 11059

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12121  df-2 12183  df-3 12184

This theorem is referenced by:  4nn  12203  3ne0  12226  3nn0  12394  3z  12500  ige3m2fz  13443  fvf1tp  13688  tpf1ofv0  14398  tpf1ofv1  14399  tpf1ofv2  14400  tpfo  14402  f1oun2prg  14819  01sqrexlem7  15150  bpoly4  15961  fsumcube  15962  sin01bnd  16089  egt2lt3  16110  rpnnen2lem2  16119  rpnnen2lem3  16120  rpnnen2lem4  16121  rpnnen2lem9  16126  rpnnen2lem11  16128  5ndvds3  16319  3lcm2e6woprm  16521  3lcm2e6  16638  prmo3  16948  5prm  17015  6nprm  17016  7prm  17017  9nprm  17019  11prm  17021  13prm  17022  17prm  17023  19prm  17024  23prm  17025  prmlem2  17026  37prm  17027  43prm  17028  83prm  17029  139prm  17030  163prm  17031  317prm  17032  631prm  17033  1259lem5  17041  2503lem1  17043  2503lem2  17044  2503lem3  17045  4001lem4  17050  4001prm  17051  mulrndx  17193  mulridx  17194  rngstr  17197  unifndx  17294  unifid  17295  unifndxnn  17296  slotsdifunifndx  17300  lt6abl  19802  cnfldstr  21288  cnfldstrOLD  21303  tangtx  26436  1cubrlem  26773  1cubr  26774  dcubic1lem  26775  dcubic2  26776  dcubic  26778  mcubic  26779  cubic2  26780  cubic  26781  quartlem3  26791  quart  26793  log2cnv  26876  log2tlbnd  26877  log2ublem1  26878  log2ublem2  26879  log2ub  26881  ppiublem1  27135  ppiub  27137  chtub  27145  bposlem3  27219  bposlem4  27220  bposlem5  27221  bposlem6  27222  bposlem9  27225  lgsdir2lem5  27262  dchrvmasumlem2  27431  dchrvmasumlema  27433  pntleml  27544  tgcgr4  28504  axlowdimlem16  28930  axlowdimlem17  28931  usgrexmpldifpr  29231  upgr3v3e3cycl  30152  ex-cnv  30409  ex-rn  30412  ex-mod  30421  2sqr3minply  33785  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  cos9thpiminplylem5  33791  fib4  34409  circlevma  34647  circlemethhgt  34648  hgt750lema  34662  sinccvglem  35708  cnndvlem1  36571  mblfinlem3  37699  itg2addnclem2  37712  itg2addnc  37714  lcm3un  42048  aks4d1p1  42109  3cubeslem2  42718  3cubeslem3r  42720  3cubes  42723  rmydioph  43047  rmxdioph  43049  expdiophlem2  43055  expdioph  43056  amgm3d  44232  lhe4.4ex1a  44362  modm2nep1  47397  modm1nep2  47399  257prm  47592  fmtno4prmfac193  47604  fmtno4nprmfac193  47605  3ndvds4  47626  139prmALT  47627  31prm  47628  127prm  47630  41prothprm  47650  341fppr2  47765  nfermltl2rev  47774  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  bgoldbtbndlem1  47836  tgoldbach  47848  grtriclwlk3  47976  gpg3kgrtriexlem2  48115  gpg3kgrtriexlem5  48118  gpg3kgrtriexlem6  48119  gpg3kgrtriex  48120