Theorem 3nn 12260

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  1c1 11039   + caddc 11041  ℕcn 12174  2c2 12236  3c3 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-2 12244  df-3 12245

This theorem is referenced by:  4nn  12264  3ne0  12287  3nn0  12455  3z  12560  ige3m2fz  13502  fvf1tp  13748  tpf1ofv0  14458  tpf1ofv1  14459  tpf1ofv2  14460  tpfo  14462  f1oun2prg  14879  01sqrexlem7  15210  bpoly4  16024  fsumcube  16025  sin01bnd  16152  egt2lt3  16173  rpnnen2lem2  16182  rpnnen2lem3  16183  rpnnen2lem4  16184  rpnnen2lem9  16189  rpnnen2lem11  16191  5ndvds3  16382  3lcm2e6woprm  16584  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  19870  cnfldstr  21354  tangtx  26469  1cubrlem  26805  1cubr  26806  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  quartlem3  26823  quart  26825  log2cnv  26908  log2tlbnd  26909  log2ublem1  26910  log2ublem2  26911  log2ub  26913  ppiublem1  27165  ppiub  27167  chtub  27175  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem9  27255  lgsdir2lem5  27292  dchrvmasumlem2  27461  dchrvmasumlema  27463  pntleml  27574  tgcgr4  28599  axlowdimlem16  29026  axlowdimlem17  29027  usgrexmpldifpr  29327  upgr3v3e3cycl  30250  ex-cnv  30507  ex-rn  30510  ex-mod  30519  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem5  33930  fib4  34548  circlevma  34786  circlemethhgt  34787  hgt750lema  34801  sinccvglem  35854  cnndvlem1  36797  mblfinlem3  37980  itg2addnclem2  37993  itg2addnc  37995  lcm3un  42454  aks4d1p1  42515  3cubeslem2  43117  3cubeslem3r  43119  3cubes  43122  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  amgm3d  44626  lhe4.4ex1a  44756  modm2nep1  47820  modm1nep2  47822  257prm  48024  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  3ndvds4  48058  139prmALT  48059  31prm  48060  127prm  48062  41prothprm  48082  341fppr2  48210  nfermltl2rev  48219  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem1  48281  tgoldbach  48293  grtriclwlk3  48421  gpg3kgrtriexlem2  48560  gpg3kgrtriexlem5  48563  gpg3kgrtriexlem6  48564  gpg3kgrtriex  48565