Theorem 2nn 9143

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 9041	. 2 |- 2 = ( 1 + 1 )
2		1nn 8993	. . 3 |- 1 e. NN
3		peano2nn 8994	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2266	1 |- 2 e. NN

Syntax hints:   e. wcel 2164  (class class class)co 5918   1c1 7873   + caddc 7875   NNcn 8982   2c2 9033

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-inn 8983  df-2 9041

This theorem is referenced by:  3nn  9144  2nn0  9257  2z  9345  uz3m2nn  9638  ige2m1fz1  10175  qbtwnre  10325  flhalf  10371  sqeq0  10673  sqeq0d  10743  facavg  10817  bcn2  10835  resqrexlemnm  11162  abs00ap  11206  geo2sum  11657  geo2lim  11659  ege2le3  11814  ef01bndlem  11899  mod2eq0even  12019  mod2eq1n2dvds  12020  sqgcd  12166  3lcm2e6woprm  12224  prm2orodd  12264  3prm  12266  4nprm  12267  isprm5lem  12279  divgcdodd  12281  isevengcd2  12296  3lcm2e6  12298  pw2dvdslemn  12303  pw2dvds  12304  pw2dvdseulemle  12305  oddpwdclemxy  12307  oddpwdclemodd  12310  oddpwdclemdc  12311  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  pythagtriplem4  12406  oddprmdvds  12492  4sqlem5  12520  4sqlem6  12521  4sqlem10  12525  4sqlem12  12540  evenennn  12550  exmidunben  12583  plusgndx  12727  plusgid  12728  plusgndxnn  12729  plusgslid  12730  grpstrg  12743  grpbaseg  12744  grpplusgg  12745  rngstrg  12752  lmodstrd  12781  topgrpstrd  12813  dsndx  12828  dsid  12829  dsslid  12830  dsndxnn  12831  slotsdifdsndx  12838  slotsdifunifndx  12845  dveflem  14872  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsval2lem  15126  lgsdir2lem2  15145  lgsdir2  15149  gausslemma2dlem1a  15174  gausslemma2dlem1cl  15175  gausslemma2dlem1f1o  15176  gausslemma2dlem4  15180  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem3  15204  2sqlem8  15210  ex-fl  15217  ex-ceil  15218  redcwlpolemeq1  15544  nconstwlpolem0  15553