Theorem 3nn 12224

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 12209	. 2 ⊢ 3 = (2 + 1)
2		2nn 12218	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12157	. . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (2 + 1) ∈ ℕ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℕ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  1c1 11027   + caddc 11029  ℕcn 12145  2c2 12200  3c3 12201

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-2 12208  df-3 12209

This theorem is referenced by:  4nn  12228  3ne0  12251  3nn0  12419  3z  12524  ige3m2fz  13464  fvf1tp  13709  tpf1ofv0  14419  tpf1ofv1  14420  tpf1ofv2  14421  tpfo  14423  f1oun2prg  14840  01sqrexlem7  15171  bpoly4  15982  fsumcube  15983  sin01bnd  16110  egt2lt3  16131  rpnnen2lem2  16140  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  rpnnen2lem11  16149  5ndvds3  16340  3lcm2e6woprm  16542  3lcm2e6  16659  prmo3  16969  5prm  17036  6nprm  17037  7prm  17038  9nprm  17040  11prm  17042  13prm  17043  17prm  17044  19prm  17045  23prm  17046  prmlem2  17047  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  4001lem4  17071  4001prm  17072  mulrndx  17214  mulridx  17215  rngstr  17218  unifndx  17315  unifid  17316  unifndxnn  17317  slotsdifunifndx  17321  lt6abl  19824  cnfldstr  21311  cnfldstrOLD  21326  tangtx  26470  1cubrlem  26807  1cubr  26808  dcubic1lem  26809  dcubic2  26810  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  quartlem3  26825  quart  26827  log2cnv  26910  log2tlbnd  26911  log2ublem1  26912  log2ublem2  26913  log2ub  26915  ppiublem1  27169  ppiub  27171  chtub  27179  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem9  27259  lgsdir2lem5  27296  dchrvmasumlem2  27465  dchrvmasumlema  27467  pntleml  27578  tgcgr4  28603  axlowdimlem16  29030  axlowdimlem17  29031  usgrexmpldifpr  29331  upgr3v3e3cycl  30255  ex-cnv  30512  ex-rn  30515  ex-mod  30524  2sqr3minply  33937  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem5  33943  fib4  34561  circlevma  34799  circlemethhgt  34800  hgt750lema  34814  sinccvglem  35866  cnndvlem1  36737  mblfinlem3  37860  itg2addnclem2  37873  itg2addnc  37875  lcm3un  42269  aks4d1p1  42330  3cubeslem2  42927  3cubeslem3r  42929  3cubes  42932  rmydioph  43256  rmxdioph  43258  expdiophlem2  43264  expdioph  43265  amgm3d  44440  lhe4.4ex1a  44570  modm2nep1  47612  modm1nep2  47614  257prm  47807  fmtno4prmfac193  47819  fmtno4nprmfac193  47820  3ndvds4  47841  139prmALT  47842  31prm  47843  127prm  47845  41prothprm  47865  341fppr2  47980  nfermltl2rev  47989  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem1  48051  tgoldbach  48063  grtriclwlk3  48191  gpg3kgrtriexlem2  48330  gpg3kgrtriexlem5  48333  gpg3kgrtriexlem6  48334  gpg3kgrtriex  48335