Theorem peano2nnd 12231

Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
peano2nnd	⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nnd

Step	Hyp	Ref	Expression
1		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		peano2nn 12226	. 2 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411  1c1 11113   + caddc 11115  ℕcn 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12215

This theorem is referenced by:  bcpasc  14283  relexpsucnnr  14974  o1fsum  15761  bpolydiflem  16000  eftlub  16054  eirrlem  16149  infpnlem1  16845  infpnlem2  16846  prmreclem4  16854  prmreclem5  16855  prmreclem6  16856  vdwlem6  16921  cayhamlem1  22375  ovolunlem1a  25020  ovolicc2lem3  25043  uniioombllem3  25109  uniioombllem4  25110  vieta1lem1  25830  vieta1lem2  25831  aaliou3lem2  25863  lgamgulmlem3  26542  lgamgulmlem4  26543  lgamgulmlem5  26544  lgamgulmlem6  26545  lgamgulm2  26547  lgamcvg2  26566  gamcvg  26567  gamcvg2lem  26570  regamcl  26572  relgamcl  26573  basellem1  26592  basellem2  26593  basellem3  26594  basellem4  26595  basellem5  26596  basellem6  26597  basellem7  26598  basellem8  26599  basellem9  26600  perfectlem1  26739  perfectlem2  26740  bclbnd  26790  lgsdilem2  26843  rplogsumlem2  26995  dchrisumlem2  27000  pntrsumbnd2  27077  pntrlog2bndlem2  27088  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  axlowdimlem16  28253  fzto1st  32303  psgnfzto1st  32305  isarchi3  32374  ofldchr  32473  smatrcl  32845  esumfzf  33136  esumpcvgval  33145  esumcvg  33153  dstfrvunirn  33542  dstfrvclim1  33545  subfacp1lem1  34239  subfacp1lem5  34244  subfaclim  34248  poimirlem7  36581  poimirlem15  36589  poimirlem17  36591  poimirlem19  36593  poimirlem28  36602  lcmineqlem11  40990  lcmineqlem18  40997  lcmineqlem19  40998  lcmineqlem20  40999  4rexfrabdioph  41618  6rexfrabdioph  41619  pellfundge  41702  pellfundgt1  41703  limsup10exlem  44567  wallispilem5  44864  wallispi2lem1  44866  wallispi2  44868  fourierdlem47  44948  nnfoctbdjlem  45250  hoidmvlelem2  45391  vonioolem2  45476  vonicclem2  45479  fmtnof1  46282  lighneallem4b  46356  proththdlem  46360  perfectALTVlem1  46468  perfectALTVlem2  46469  blennngt2o2  47356