Theorem 2nn 9421

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 9318	. 2 |- 2 = ( 1 + 1 )
2		1nn 9270	. . 3 |- 1 e. NN
3		peano2nn 9271	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2307	1 |- 2 e. NN

Syntax hints:   e. wcel 2205  (class class class)co 6060   1c1 8146   + caddc 8148   NNcn 9259   2c2 9310

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4234  ax-cnex 8236  ax-resscn 8237  ax-1re 8239  ax-addrcl 8242

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-int 3956  df-br 4116  df-iota 5319  df-fv 5367  df-ov 6063  df-inn 9260  df-2 9318

This theorem is referenced by:  3nn  9422  2nn0  9535  2z  9627  uz3m2nn  9928  ige2m1fz1  10470  qbtwnre  10645  flhalf  10691  sqeq0  10993  sqeq0d  11064  facavg  11138  bcn2  11156  resqrexlemnm  11734  abs00ap  11778  geo2sum  12231  geo2lim  12233  ege2le3  12388  ef01bndlem  12473  mod2eq0even  12595  mod2eq1n2dvds  12596  bitsdc  12664  bits0o  12667  bitsp1  12668  bitsp1o  12670  bitsfzolem  12671  bitsfzo  12672  bitsmod  12673  bitsfi  12674  bitscmp  12675  bitsinv1lem  12678  bitsinv1  12679  sqgcd  12756  3lcm2e6woprm  12814  prm2orodd  12854  3prm  12856  4nprm  12857  isprm5lem  12869  divgcdodd  12871  isevengcd2  12886  3lcm2e6  12888  pw2dvdslemn  12893  pw2dvds  12894  pw2dvdseulemle  12895  oddpwdclemxy  12897  oddpwdclemodd  12900  oddpwdclemdc  12901  oddpwdc  12902  sqpweven  12903  2sqpwodd  12904  pythagtriplem4  12997  oddprmdvds  13083  4sqlem5  13111  4sqlem6  13112  4sqlem10  13116  4sqlem12  13131  dec2dvds  13140  dec5nprm  13143  dec2nprm  13144  2expltfac  13168  evenennn  13234  exmidunben  13267  plusgndx  13412  plusgid  13413  plusgndxnn  13414  plusgslid  13415  grpstrg  13429  grpbaseg  13430  grpplusgg  13431  rngstrg  13438  lmodstrd  13467  topgrpstrd  13499  dsndx  13518  dsid  13519  dsslid  13520  dsndxnn  13521  slotsdifdsndx  13528  slotsdifunifndx  13535  imasvalstrd  13568  cnfldstr  14839  dveflem  15722  1sgm2ppw  15994  mersenne  15996  perfect1  15997  perfectlem1  15998  perfectlem2  15999  perfect  16000  lgsval  16008  lgsfvalg  16009  lgsfcl2  16010  lgsval2lem  16014  lgsdir2lem2  16033  lgsdir2  16037  gausslemma2dlem1a  16062  gausslemma2dlem1cl  16063  gausslemma2dlem1f1o  16064  gausslemma2dlem4  16068  gausslemma2d  16073  lgseisenlem1  16074  lgseisenlem2  16075  lgseisenlem3  16076  lgseisenlem4  16077  lgsquadlemofi  16080  lgsquadlem1  16081  lgsquadlem2  16082  lgsquad2lem2  16086  m1lgs  16089  2lgslem1c  16094  2lgslem3a1  16101  2lgslem3d1  16104  2lgslem4  16107  2lgs  16108  2sqlem3  16121  2sqlem8  16127  clwwlkn2  16547  eupth2lem3lem4fi  16599  konigsberglem5  16618  ex-fl  16624  ex-ceil  16625  redcwlpolemeq1  16980  nconstwlpolem0  16989