Theorem 2nn 8977

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 8875	. 2 |- 2 = ( 1 + 1 )
2		1nn 8827	. . 3 |- 1 e. NN
3		peano2nn 8828	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2230	1 |- 2 e. NN

Syntax hints:   e. wcel 2128  (class class class)co 5818   1c1 7716   + caddc 7718   NNcn 8816   2c2 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4082  ax-cnex 7806  ax-resscn 7807  ax-1re 7809  ax-addrcl 7812

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-iota 5132  df-fv 5175  df-ov 5821  df-inn 8817  df-2 8875

This theorem is referenced by:  3nn  8978  2nn0  9090  2z  9178  uz3m2nn  9467  ige2m1fz1  9993  qbtwnre  10138  flhalf  10183  sqeq0  10464  sqeq0d  10532  facavg  10602  bcn2  10620  resqrexlemnm  10900  abs00ap  10944  geo2sum  11393  geo2lim  11395  ege2le3  11550  ef01bndlem  11635  mod2eq0even  11750  mod2eq1n2dvds  11751  sqgcd  11893  3lcm2e6woprm  11943  prm2orodd  11983  3prm  11985  4nprm  11986  divgcdodd  11997  isevengcd2  12012  3lcm2e6  12014  pw2dvdslemn  12019  pw2dvds  12020  pw2dvdseulemle  12021  oddpwdclemxy  12023  oddpwdclemodd  12026  oddpwdclemdc  12027  oddpwdc  12028  sqpweven  12029  2sqpwodd  12030  evenennn  12094  exmidunben  12127  plusgndx  12243  plusgid  12244  plusgslid  12245  grpstrg  12257  grpbaseg  12258  grpplusgg  12259  rngstrg  12265  lmodstrd  12283  topgrpstrd  12301  dsndx  12308  dsid  12309  dsslid  12310  dveflem  13047  ex-fl  13261  ex-ceil  13262  redcwlpolemeq1  13588  nconstwlpolem0  13596