Theorem 2nn 9115

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 9013	. 2 ⊢ 2 = (1 + 1)
2		1nn 8965	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 8966	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2262	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2160  (class class class)co 5900  1c1 7847   + caddc 7849  ℕcn 8954  2c2 9005

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 2171  ax-sep 4139  ax-cnex 7937  ax-resscn 7938  ax-1re 7940  ax-addrcl 7943

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-int 3863  df-br 4022  df-iota 5199  df-fv 5246  df-ov 5903  df-inn 8955  df-2 9013

This theorem is referenced by:  3nn  9116  2nn0  9228  2z  9316  uz3m2nn  9609  ige2m1fz1  10145  qbtwnre  10293  flhalf  10339  sqeq0  10623  sqeq0d  10693  facavg  10767  bcn2  10785  resqrexlemnm  11068  abs00ap  11112  geo2sum  11563  geo2lim  11565  ege2le3  11720  ef01bndlem  11805  mod2eq0even  11924  mod2eq1n2dvds  11925  sqgcd  12071  3lcm2e6woprm  12129  prm2orodd  12169  3prm  12171  4nprm  12172  isprm5lem  12184  divgcdodd  12186  isevengcd2  12201  3lcm2e6  12203  pw2dvdslemn  12208  pw2dvds  12209  pw2dvdseulemle  12210  oddpwdclemxy  12212  oddpwdclemodd  12215  oddpwdclemdc  12216  oddpwdc  12217  sqpweven  12218  2sqpwodd  12219  pythagtriplem4  12311  oddprmdvds  12397  4sqlem5  12425  4sqlem6  12426  4sqlem10  12430  4sqlem12  12445  evenennn  12455  exmidunben  12488  plusgndx  12632  plusgid  12633  plusgndxnn  12634  plusgslid  12635  grpstrg  12648  grpbaseg  12649  grpplusgg  12650  rngstrg  12657  lmodstrd  12686  topgrpstrd  12718  dsndx  12733  dsid  12734  dsslid  12735  dsndxnn  12736  slotsdifdsndx  12743  slotsdifunifndx  12750  dveflem  14672  lgsval  14891  lgsfvalg  14892  lgsfcl2  14893  lgsval2lem  14897  lgsdir2lem2  14916  lgsdir2  14920  lgseisenlem1  14936  lgseisenlem2  14937  m1lgs  14938  2sqlem3  14950  2sqlem8  14956  ex-fl  14963  ex-ceil  14964  redcwlpolemeq1  15290  nconstwlpolem0  15299