Theorem 2nn 9304

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 9201	. 2 ⊢ 2 = (1 + 1)
2		1nn 9153	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9154	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2304	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  1c1 8032   + caddc 8034  ℕcn 9142  2c2 9193

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

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 6020  df-inn 9143  df-2 9201

This theorem is referenced by:  3nn  9305  2nn0  9418  2z  9506  uz3m2nn  9806  ige2m1fz1  10343  qbtwnre  10515  flhalf  10561  sqeq0  10863  sqeq0d  10933  facavg  11007  bcn2  11025  resqrexlemnm  11578  abs00ap  11622  geo2sum  12074  geo2lim  12076  ege2le3  12231  ef01bndlem  12316  mod2eq0even  12438  mod2eq1n2dvds  12439  bitsdc  12507  bits0o  12510  bitsp1  12511  bitsp1o  12513  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitsfi  12517  bitscmp  12518  bitsinv1lem  12521  bitsinv1  12522  sqgcd  12599  3lcm2e6woprm  12657  prm2orodd  12697  3prm  12699  4nprm  12700  isprm5lem  12712  divgcdodd  12714  isevengcd2  12729  3lcm2e6  12731  pw2dvdslemn  12736  pw2dvds  12737  pw2dvdseulemle  12738  oddpwdclemxy  12740  oddpwdclemodd  12743  oddpwdclemdc  12744  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  pythagtriplem4  12840  oddprmdvds  12926  4sqlem5  12954  4sqlem6  12955  4sqlem10  12959  4sqlem12  12974  dec2dvds  12983  dec5nprm  12986  dec2nprm  12987  2expltfac  13011  evenennn  13013  exmidunben  13046  plusgndx  13191  plusgid  13192  plusgndxnn  13193  plusgslid  13194  grpstrg  13208  grpbaseg  13209  grpplusgg  13210  rngstrg  13217  lmodstrd  13246  topgrpstrd  13278  dsndx  13297  dsid  13298  dsslid  13299  dsndxnn  13300  slotsdifdsndx  13307  slotsdifunifndx  13314  imasvalstrd  13352  cnfldstr  14571  dveflem  15449  1sgm2ppw  15718  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgsval2lem  15738  lgsdir2lem2  15757  lgsdir2  15761  gausslemma2dlem1a  15786  gausslemma2dlem1cl  15787  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlemofi  15804  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  m1lgs  15813  2lgslem1c  15818  2lgslem3a1  15825  2lgslem3d1  15828  2lgslem4  15831  2lgs  15832  2sqlem3  15845  2sqlem8  15851  clwwlkn2  16271  ex-fl  16321  ex-ceil  16322  redcwlpolemeq1  16658  nconstwlpolem0  16667