Theorem 2nn 9305

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

Assertion

Ref	Expression
2nn	|- 2 e. NN

Proof of Theorem 2nn

Step	Hyp	Ref	Expression
1		df-2 9202	. 2 |- 2 = ( 1 + 1 )
2		1nn 9154	. . 3 |- 1 e. NN
3		peano2nn 9155	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2304	1 |- 2 e. NN

Syntax hints:   e. wcel 2202  (class class class)co 6018   1c1 8033   + caddc 8035   NNcn 9143   2c2 9194

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-inn 9144  df-2 9202

This theorem is referenced by:  3nn  9306  2nn0  9419  2z  9507  uz3m2nn  9807  ige2m1fz1  10344  qbtwnre  10517  flhalf  10563  sqeq0  10865  sqeq0d  10935  facavg  11009  bcn2  11027  resqrexlemnm  11596  abs00ap  11640  geo2sum  12093  geo2lim  12095  ege2le3  12250  ef01bndlem  12335  mod2eq0even  12457  mod2eq1n2dvds  12458  bitsdc  12526  bits0o  12529  bitsp1  12530  bitsp1o  12532  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitsfi  12536  bitscmp  12537  bitsinv1lem  12540  bitsinv1  12541  sqgcd  12618  3lcm2e6woprm  12676  prm2orodd  12716  3prm  12718  4nprm  12719  isprm5lem  12731  divgcdodd  12733  isevengcd2  12748  3lcm2e6  12750  pw2dvdslemn  12755  pw2dvds  12756  pw2dvdseulemle  12757  oddpwdclemxy  12759  oddpwdclemodd  12762  oddpwdclemdc  12763  oddpwdc  12764  sqpweven  12765  2sqpwodd  12766  pythagtriplem4  12859  oddprmdvds  12945  4sqlem5  12973  4sqlem6  12974  4sqlem10  12978  4sqlem12  12993  dec2dvds  13002  dec5nprm  13005  dec2nprm  13006  2expltfac  13030  evenennn  13032  exmidunben  13065  plusgndx  13210  plusgid  13211  plusgndxnn  13212  plusgslid  13213  grpstrg  13227  grpbaseg  13228  grpplusgg  13229  rngstrg  13236  lmodstrd  13265  topgrpstrd  13297  dsndx  13316  dsid  13317  dsslid  13318  dsndxnn  13319  slotsdifdsndx  13326  slotsdifunifndx  13333  imasvalstrd  13371  cnfldstr  14591  dveflem  15469  1sgm2ppw  15738  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgsval2lem  15758  lgsdir2lem2  15777  lgsdir2  15781  gausslemma2dlem1a  15806  gausslemma2dlem1cl  15807  gausslemma2dlem1f1o  15808  gausslemma2dlem4  15812  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlemofi  15824  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  m1lgs  15833  2lgslem1c  15838  2lgslem3a1  15845  2lgslem3d1  15848  2lgslem4  15851  2lgs  15852  2sqlem3  15865  2sqlem8  15871  clwwlkn2  16291  eupth2lem3lem4fi  16343  konigsberglem5  16362  ex-fl  16368  ex-ceil  16369  redcwlpolemeq1  16710  nconstwlpolem0  16719