Theorem 2nn 9295

Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)

Assertion

Ref	Expression
2nn	⊢ 2 ∈ ℕ

Proof of Theorem 2nn

Step	Hyp	Ref	Expression
1		df-2 9192	. 2 ⊢ 2 = (1 + 1)
2		1nn 9144	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9145	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2302	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  1c1 8023   + caddc 8025  ℕcn 9133  2c2 9184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-inn 9134  df-2 9192

This theorem is referenced by:  3nn  9296  2nn0  9409  2z  9497  uz3m2nn  9797  ige2m1fz1  10334  qbtwnre  10506  flhalf  10552  sqeq0  10854  sqeq0d  10924  facavg  10998  bcn2  11016  resqrexlemnm  11569  abs00ap  11613  geo2sum  12065  geo2lim  12067  ege2le3  12222  ef01bndlem  12307  mod2eq0even  12429  mod2eq1n2dvds  12430  bitsdc  12498  bits0o  12501  bitsp1  12502  bitsp1o  12504  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitsfi  12508  bitscmp  12509  bitsinv1lem  12512  bitsinv1  12513  sqgcd  12590  3lcm2e6woprm  12648  prm2orodd  12688  3prm  12690  4nprm  12691  isprm5lem  12703  divgcdodd  12705  isevengcd2  12720  3lcm2e6  12722  pw2dvdslemn  12727  pw2dvds  12728  pw2dvdseulemle  12729  oddpwdclemxy  12731  oddpwdclemodd  12734  oddpwdclemdc  12735  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  pythagtriplem4  12831  oddprmdvds  12917  4sqlem5  12945  4sqlem6  12946  4sqlem10  12950  4sqlem12  12965  dec2dvds  12974  dec5nprm  12977  dec2nprm  12978  2expltfac  13002  evenennn  13004  exmidunben  13037  plusgndx  13182  plusgid  13183  plusgndxnn  13184  plusgslid  13185  grpstrg  13199  grpbaseg  13200  grpplusgg  13201  rngstrg  13208  lmodstrd  13237  topgrpstrd  13269  dsndx  13288  dsid  13289  dsslid  13290  dsndxnn  13291  slotsdifdsndx  13298  slotsdifunifndx  13305  imasvalstrd  13343  cnfldstr  14562  dveflem  15440  1sgm2ppw  15709  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgsval2lem  15729  lgsdir2lem2  15748  lgsdir2  15752  gausslemma2dlem1a  15777  gausslemma2dlem1cl  15778  gausslemma2dlem1f1o  15779  gausslemma2dlem4  15783  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlemofi  15795  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  m1lgs  15804  2lgslem1c  15809  2lgslem3a1  15816  2lgslem3d1  15819  2lgslem4  15822  2lgs  15823  2sqlem3  15836  2sqlem8  15842  clwwlkn2  16216  ex-fl  16257  ex-ceil  16258  redcwlpolemeq1  16594  nconstwlpolem0  16603