Theorem 2nn 9218

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 9115	. 2 ⊢ 2 = (1 + 1)
2		1nn 9067	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9068	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2279	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2177  (class class class)co 5957  1c1 7946   + caddc 7948  ℕcn 9056  2c2 9107

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4170  ax-cnex 8036  ax-resscn 8037  ax-1re 8039  ax-addrcl 8042

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-int 3892  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960  df-inn 9057  df-2 9115

This theorem is referenced by:  3nn  9219  2nn0  9332  2z  9420  uz3m2nn  9714  ige2m1fz1  10251  qbtwnre  10421  flhalf  10467  sqeq0  10769  sqeq0d  10839  facavg  10913  bcn2  10931  resqrexlemnm  11404  abs00ap  11448  geo2sum  11900  geo2lim  11902  ege2le3  12057  ef01bndlem  12142  mod2eq0even  12264  mod2eq1n2dvds  12265  bitsdc  12333  bits0o  12336  bitsp1  12337  bitsp1o  12339  bitsfzolem  12340  bitsfzo  12341  bitsmod  12342  bitsfi  12343  bitscmp  12344  bitsinv1lem  12347  bitsinv1  12348  sqgcd  12425  3lcm2e6woprm  12483  prm2orodd  12523  3prm  12525  4nprm  12526  isprm5lem  12538  divgcdodd  12540  isevengcd2  12555  3lcm2e6  12557  pw2dvdslemn  12562  pw2dvds  12563  pw2dvdseulemle  12564  oddpwdclemxy  12566  oddpwdclemodd  12569  oddpwdclemdc  12570  oddpwdc  12571  sqpweven  12572  2sqpwodd  12573  pythagtriplem4  12666  oddprmdvds  12752  4sqlem5  12780  4sqlem6  12781  4sqlem10  12785  4sqlem12  12800  dec2dvds  12809  dec5nprm  12812  dec2nprm  12813  2expltfac  12837  evenennn  12839  exmidunben  12872  plusgndx  13016  plusgid  13017  plusgndxnn  13018  plusgslid  13019  grpstrg  13033  grpbaseg  13034  grpplusgg  13035  rngstrg  13042  lmodstrd  13071  topgrpstrd  13103  dsndx  13122  dsid  13123  dsslid  13124  dsndxnn  13125  slotsdifdsndx  13132  slotsdifunifndx  13139  imasvalstrd  13177  cnfldstr  14395  dveflem  15273  1sgm2ppw  15542  mersenne  15544  perfect1  15545  perfectlem1  15546  perfectlem2  15547  perfect  15548  lgsval  15556  lgsfvalg  15557  lgsfcl2  15558  lgsval2lem  15562  lgsdir2lem2  15581  lgsdir2  15585  gausslemma2dlem1a  15610  gausslemma2dlem1cl  15611  gausslemma2dlem1f1o  15612  gausslemma2dlem4  15616  gausslemma2d  15621  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgsquadlemofi  15628  lgsquadlem1  15629  lgsquadlem2  15630  lgsquad2lem2  15634  m1lgs  15637  2lgslem1c  15642  2lgslem3a1  15649  2lgslem3d1  15652  2lgslem4  15655  2lgs  15656  2sqlem3  15669  2sqlem8  15675  ex-fl  15800  ex-ceil  15801  redcwlpolemeq1  16134  nconstwlpolem0  16143