Theorem 2nn 9026

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 8924	. 2 ⊢ 2 = (1 + 1)
2		1nn 8876	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 8877	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2243	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2141  (class class class)co 5850  1c1 7762   + caddc 7764  ℕcn 8865  2c2 8916

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105  ax-cnex 7852  ax-resscn 7853  ax-1re 7855  ax-addrcl 7858

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853  df-inn 8866  df-2 8924

This theorem is referenced by:  3nn  9027  2nn0  9139  2z  9227  uz3m2nn  9519  ige2m1fz1  10052  qbtwnre  10200  flhalf  10245  sqeq0  10526  sqeq0d  10595  facavg  10667  bcn2  10685  resqrexlemnm  10969  abs00ap  11013  geo2sum  11464  geo2lim  11466  ege2le3  11621  ef01bndlem  11706  mod2eq0even  11824  mod2eq1n2dvds  11825  sqgcd  11971  3lcm2e6woprm  12027  prm2orodd  12067  3prm  12069  4nprm  12070  isprm5lem  12082  divgcdodd  12084  isevengcd2  12099  3lcm2e6  12101  pw2dvdslemn  12106  pw2dvds  12107  pw2dvdseulemle  12108  oddpwdclemxy  12110  oddpwdclemodd  12113  oddpwdclemdc  12114  oddpwdc  12115  sqpweven  12116  2sqpwodd  12117  pythagtriplem4  12209  oddprmdvds  12293  4sqlem5  12321  4sqlem6  12322  4sqlem10  12326  evenennn  12335  exmidunben  12368  plusgndx  12497  plusgid  12498  plusgslid  12499  grpstrg  12511  grpbaseg  12512  grpplusgg  12513  rngstrg  12519  lmodstrd  12537  topgrpstrd  12555  dsndx  12562  dsid  12563  dsslid  12564  dveflem  13402  lgsval  13620  lgsfvalg  13621  lgsfcl2  13622  lgsval2lem  13626  lgsdir2lem2  13645  lgsdir2  13649  2sqlem3  13668  2sqlem8  13674  ex-fl  13681  ex-ceil  13682  redcwlpolemeq1  14008  nconstwlpolem0  14016