Theorem peano2nnd 12226

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 12221	. 2 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7406  1c1 11108   + caddc 11110  ℕcn 12209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-nn 12210

This theorem is referenced by:  bcpasc  14278  relexpsucnnr  14969  o1fsum  15756  bpolydiflem  15995  eftlub  16049  eirrlem  16144  infpnlem1  16840  infpnlem2  16841  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  vdwlem6  16916  cayhamlem1  22360  ovolunlem1a  25005  ovolicc2lem3  25028  uniioombllem3  25094  uniioombllem4  25095  vieta1lem1  25815  vieta1lem2  25816  aaliou3lem2  25848  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamgulm2  26530  lgamcvg2  26549  gamcvg  26550  gamcvg2lem  26553  regamcl  26555  relgamcl  26556  basellem1  26575  basellem2  26576  basellem3  26577  basellem4  26578  basellem5  26579  basellem6  26580  basellem7  26581  basellem8  26582  basellem9  26583  perfectlem1  26722  perfectlem2  26723  bclbnd  26773  lgsdilem2  26826  rplogsumlem2  26978  dchrisumlem2  26983  pntrsumbnd2  27060  pntrlog2bndlem2  27071  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  axlowdimlem16  28205  fzto1st  32250  psgnfzto1st  32252  isarchi3  32321  ofldchr  32421  smatrcl  32765  esumfzf  33056  esumpcvgval  33065  esumcvg  33073  dstfrvunirn  33462  dstfrvclim1  33465  subfacp1lem1  34159  subfacp1lem5  34164  subfaclim  34168  poimirlem7  36484  poimirlem15  36492  poimirlem17  36494  poimirlem19  36496  poimirlem28  36505  lcmineqlem11  40893  lcmineqlem18  40900  lcmineqlem19  40901  lcmineqlem20  40902  4rexfrabdioph  41522  6rexfrabdioph  41523  pellfundge  41606  pellfundgt1  41607  limsup10exlem  44475  wallispilem5  44772  wallispi2lem1  44774  wallispi2  44776  fourierdlem47  44856  nnfoctbdjlem  45158  hoidmvlelem2  45299  vonioolem2  45384  vonicclem2  45387  fmtnof1  46190  lighneallem4b  46264  proththdlem  46268  perfectALTVlem1  46376  perfectALTVlem2  46377  blennngt2o2  47232