Theorem 3nn 12347

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 12332	. 2 ⊢ 3 = (2 + 1)
2		2nn 12341	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12280	. . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (2 + 1) ∈ ℕ
5	1, 4	eqeltri 2825	1 ⊢ 3 ∈ ℕ

Syntax hints:   ∈ wcel 2100  (class class class)co 7427  1c1 11160   + caddc 11162  ℕcn 12268  2c2 12323  3c3 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pr 5435  ax-un 7748  ax-1cn 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-pss 3978  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-ov 7430  df-om 7882  df-2nd 8009  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-nn 12269  df-2 12331  df-3 12332

This theorem is referenced by:  4nn  12351  3nn0  12546  3z  12651  ige3m2fz  13583  fvf1tp  13814  tpf1ofv0  14518  tpf1ofv1  14519  tpf1ofv2  14520  tpfo  14522  f1oun2prg  14939  01sqrexlem7  15266  bpoly4  16074  fsumcube  16075  sin01bnd  16200  egt2lt3  16221  rpnnen2lem2  16230  rpnnen2lem3  16231  rpnnen2lem4  16232  rpnnen2lem9  16237  rpnnen2lem11  16239  3lcm2e6woprm  16629  3lcm2e6  16747  prmo3  17056  5prm  17124  6nprm  17125  7prm  17126  9nprm  17128  11prm  17130  13prm  17131  17prm  17132  19prm  17133  23prm  17134  prmlem2  17135  37prm  17136  43prm  17137  83prm  17138  139prm  17139  163prm  17140  317prm  17141  631prm  17142  1259lem5  17150  2503lem1  17152  2503lem2  17153  2503lem3  17154  4001lem4  17159  4001prm  17160  mulrndx  17320  mulridx  17321  rngstr  17325  unifndx  17422  unifid  17423  unifndxnn  17424  slotsdifunifndx  17428  lt6abl  19905  sramulrOLD  21173  cnfldstr  21357  cnfldstrOLD  21372  cnfldfunALTOLDOLD  21384  zlmmulrOLD  21525  znmulOLD  21551  opsrmulrOLD  22064  tuslemOLD  24263  tngmulrOLD  24648  tangtx  26530  1cubrlem  26866  1cubr  26867  dcubic1lem  26868  dcubic2  26869  dcubic  26871  mcubic  26872  cubic2  26873  cubic  26874  quartlem3  26884  quart  26886  log2cnv  26969  log2tlbnd  26970  log2ublem1  26971  log2ublem2  26972  log2ub  26974  ppiublem1  27228  ppiub  27230  chtub  27238  bposlem3  27312  bposlem4  27313  bposlem5  27314  bposlem6  27315  bposlem9  27318  lgsdir2lem5  27355  dchrvmasumlem2  27524  dchrvmasumlema  27526  pntleml  27637  tgcgr4  28455  axlowdimlem16  28888  axlowdimlem17  28889  usgrexmpldifpr  29191  upgr3v3e3cycl  30110  ex-cnv  30367  ex-rn  30370  ex-mod  30379  resvmulrOLD  33231  2sqr3minply  33638  fib4  34269  circlevma  34519  circlemethhgt  34520  hgt750lema  34534  sinccvglem  35540  cnndvlem1  36281  mblfinlem3  37400  itg2addnclem2  37413  itg2addnc  37415  hlhilsmulOLD  41684  lcm3un  41754  aks4d1p1  41815  3cubeslem2  42409  3cubeslem3r  42411  3cubes  42414  rmydioph  42739  rmxdioph  42741  expdiophlem2  42747  expdioph  42748  amgm3d  43933  lhe4.4ex1a  44070  257prm  47199  fmtno4prmfac193  47211  fmtno4nprmfac193  47212  3ndvds4  47233  139prmALT  47234  31prm  47235  127prm  47237  41prothprm  47257  341fppr2  47372  nfermltl2rev  47381  wtgoldbnnsum4prm  47440  bgoldbnnsum3prm  47442  bgoldbtbndlem1  47443  tgoldbach  47455  grtriclwlk3  47584