Theorem 2nn 8675

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 8579	. 2 ⊢ 2 = (1 + 1)
2		1nn 8531	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 8532	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 7	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2167	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 1445  (class class class)co 5690  1c1 7448   + caddc 7450  ℕcn 8520  2c2 8571

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-cnex 7533  ax-resscn 7534  ax-1re 7536  ax-addrcl 7539

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693  df-inn 8521  df-2 8579

This theorem is referenced by:  3nn  8676  2nn0  8788  2z  8876  uz3m2nn  9160  ige2m1fz1  9672  qbtwnre  9817  flhalf  9858  sqeq0  10149  sqeq0d  10216  facavg  10285  bcn2  10303  resqrexlemnm  10582  abs00ap  10626  geo2sum  11072  geo2lim  11074  ege2le3  11125  ef01bndlem  11211  mod2eq0even  11320  mod2eq1n2dvds  11321  sqgcd  11460  3lcm2e6woprm  11510  prm2orodd  11550  3prm  11552  4nprm  11553  divgcdodd  11564  isevengcd2  11579  3lcm2e6  11581  pw2dvdslemn  11585  pw2dvds  11586  pw2dvdseulemle  11587  oddpwdclemxy  11589  oddpwdclemodd  11592  oddpwdclemdc  11593  oddpwdc  11594  sqpweven  11595  2sqpwodd  11596  evenennn  11648  plusgndx  11751  plusgid  11752  plusgslid  11753  grpstrg  11765  grpbaseg  11766  grpplusgg  11767  rngstrg  11773  lmodstrd  11791  topgrpstrd  11809  dsndx  11816  dsid  11817  dsslid  11818  ex-fl  12364  ex-ceil  12365