Theorem 3nn 12195

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 12180	. 2 ⊢ 3 = (2 + 1)
2		2nn 12189	. . 3 ⊢ 2 ∈ ℕ
3		peano2nn 12128	. . 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 7340  1c1 10998   + caddc 11000  ℕcn 12116  2c2 12171  3c3 12172

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 5231  ax-nul 5241  ax-pr 5367  ax-un 7662  ax-1cn 11055

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 3344  df-rab 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4940  df-br 5089  df-opab 5151  df-mpt 5170  df-tr 5196  df-id 5508  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5566  df-we 5568  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  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 7343  df-om 7791  df-2nd 7916  df-frecs 8205  df-wrecs 8236  df-recs 8285  df-rdg 8323  df-nn 12117  df-2 12179  df-3 12180

This theorem is referenced by:  4nn  12199  3ne0  12222  3nn0  12390  3z  12496  ige3m2fz  13439  fvf1tp  13681  tpf1ofv0  14391  tpf1ofv1  14392  tpf1ofv2  14393  tpfo  14395  f1oun2prg  14811  01sqrexlem7  15142  bpoly4  15953  fsumcube  15954  sin01bnd  16081  egt2lt3  16102  rpnnen2lem2  16111  rpnnen2lem3  16112  rpnnen2lem4  16113  rpnnen2lem9  16118  rpnnen2lem11  16120  5ndvds3  16311  3lcm2e6woprm  16513  3lcm2e6  16630  prmo3  16940  5prm  17007  6nprm  17008  7prm  17009  9nprm  17011  11prm  17013  13prm  17014  17prm  17015  19prm  17016  23prm  17017  prmlem2  17018  37prm  17019  43prm  17020  83prm  17021  139prm  17022  163prm  17023  317prm  17024  631prm  17025  1259lem5  17033  2503lem1  17035  2503lem2  17036  2503lem3  17037  4001lem4  17042  4001prm  17043  mulrndx  17185  mulridx  17186  rngstr  17189  unifndx  17286  unifid  17287  unifndxnn  17288  slotsdifunifndx  17292  lt6abl  19761  cnfldstr  21247  cnfldstrOLD  21262  tangtx  26395  1cubrlem  26732  1cubr  26733  dcubic1lem  26734  dcubic2  26735  dcubic  26737  mcubic  26738  cubic2  26739  cubic  26740  quartlem3  26750  quart  26752  log2cnv  26835  log2tlbnd  26836  log2ublem1  26837  log2ublem2  26838  log2ub  26840  ppiublem1  27094  ppiub  27096  chtub  27104  bposlem3  27178  bposlem4  27179  bposlem5  27180  bposlem6  27181  bposlem9  27184  lgsdir2lem5  27221  dchrvmasumlem2  27390  dchrvmasumlema  27392  pntleml  27503  tgcgr4  28463  axlowdimlem16  28889  axlowdimlem17  28890  usgrexmpldifpr  29190  upgr3v3e3cycl  30111  ex-cnv  30368  ex-rn  30371  ex-mod  30380  2sqr3minply  33761  cos9thpiminplylem1  33763  cos9thpiminplylem2  33764  cos9thpiminplylem5  33767  fib4  34385  circlevma  34623  circlemethhgt  34624  hgt750lema  34638  sinccvglem  35662  cnndvlem1  36528  mblfinlem3  37656  itg2addnclem2  37669  itg2addnc  37671  lcm3un  42005  aks4d1p1  42066  3cubeslem2  42675  3cubeslem3r  42677  3cubes  42680  rmydioph  43004  rmxdioph  43006  expdiophlem2  43012  expdioph  43013  amgm3d  44189  lhe4.4ex1a  44319  modm2nep1  47364  modm1nep2  47366  257prm  47559  fmtno4prmfac193  47571  fmtno4nprmfac193  47572  3ndvds4  47593  139prmALT  47594  31prm  47595  127prm  47597  41prothprm  47617  341fppr2  47732  nfermltl2rev  47741  wtgoldbnnsum4prm  47800  bgoldbnnsum3prm  47802  bgoldbtbndlem1  47803  tgoldbach  47815  grtriclwlk3  47943  gpg3kgrtriexlem2  48082  gpg3kgrtriexlem5  48085  gpg3kgrtriexlem6  48086  gpg3kgrtriex  48087