Theorem 3nn 12265

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 12250	. 2 ⊢ 3 = (2 + 1)
2		2nn 12259	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12198	. . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (2 + 1) ∈ ℕ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  1c1 11069   + caddc 11071  ℕcn 12186  2c2 12241  3c3 12242

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-2 12249  df-3 12250

This theorem is referenced by:  4nn  12269  3ne0  12292  3nn0  12460  3z  12566  ige3m2fz  13509  fvf1tp  13751  tpf1ofv0  14461  tpf1ofv1  14462  tpf1ofv2  14463  tpfo  14465  f1oun2prg  14883  01sqrexlem7  15214  bpoly4  16025  fsumcube  16026  sin01bnd  16153  egt2lt3  16174  rpnnen2lem2  16183  rpnnen2lem3  16184  rpnnen2lem4  16185  rpnnen2lem9  16190  rpnnen2lem11  16192  5ndvds3  16383  3lcm2e6woprm  16585  3lcm2e6  16702  prmo3  17012  5prm  17079  6nprm  17080  7prm  17081  9nprm  17083  11prm  17085  13prm  17086  17prm  17087  19prm  17088  23prm  17089  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem4  17114  4001prm  17115  mulrndx  17257  mulridx  17258  rngstr  17261  unifndx  17358  unifid  17359  unifndxnn  17360  slotsdifunifndx  17364  lt6abl  19825  cnfldstr  21266  cnfldstrOLD  21281  tangtx  26414  1cubrlem  26751  1cubr  26752  dcubic1lem  26753  dcubic2  26754  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  quartlem3  26769  quart  26771  log2cnv  26854  log2tlbnd  26855  log2ublem1  26856  log2ublem2  26857  log2ub  26859  ppiublem1  27113  ppiub  27115  chtub  27123  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem9  27203  lgsdir2lem5  27240  dchrvmasumlem2  27409  dchrvmasumlema  27411  pntleml  27522  tgcgr4  28458  axlowdimlem16  28884  axlowdimlem17  28885  usgrexmpldifpr  29185  upgr3v3e3cycl  30109  ex-cnv  30366  ex-rn  30369  ex-mod  30378  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem5  33776  fib4  34395  circlevma  34633  circlemethhgt  34634  hgt750lema  34648  sinccvglem  35659  cnndvlem1  36525  mblfinlem3  37653  itg2addnclem2  37666  itg2addnc  37668  lcm3un  42003  aks4d1p1  42064  3cubeslem2  42673  3cubeslem3r  42675  3cubes  42678  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  amgm3d  44188  lhe4.4ex1a  44318  modm2nep1  47367  modm1nep2  47369  257prm  47562  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  3ndvds4  47596  139prmALT  47597  31prm  47598  127prm  47600  41prothprm  47620  341fppr2  47735  nfermltl2rev  47744  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem1  47806  tgoldbach  47818  grtriclwlk3  47944  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem5  48078  gpg3kgrtriexlem6  48079  gpg3kgrtriex  48080