Theorem peano2nnd 12234

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7412  1c1 11115   + caddc 11117  ℕcn 12217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  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 7415  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-nn 12218

This theorem is referenced by:  bcpasc  14286  relexpsucnnr  14977  o1fsum  15764  bpolydiflem  16003  eftlub  16057  eirrlem  16152  infpnlem1  16848  infpnlem2  16849  prmreclem4  16857  prmreclem5  16858  prmreclem6  16859  vdwlem6  16924  cayhamlem1  22589  ovolunlem1a  25246  ovolicc2lem3  25269  uniioombllem3  25335  uniioombllem4  25336  vieta1lem1  26060  vieta1lem2  26061  aaliou3lem2  26093  lgamgulmlem3  26772  lgamgulmlem4  26773  lgamgulmlem5  26774  lgamgulmlem6  26775  lgamgulm2  26777  lgamcvg2  26796  gamcvg  26797  gamcvg2lem  26800  regamcl  26802  relgamcl  26803  basellem1  26822  basellem2  26823  basellem3  26824  basellem4  26825  basellem5  26826  basellem6  26827  basellem7  26828  basellem8  26829  basellem9  26830  perfectlem1  26969  perfectlem2  26970  bclbnd  27020  lgsdilem2  27073  rplogsumlem2  27225  dchrisumlem2  27230  pntrsumbnd2  27307  pntrlog2bndlem2  27318  pntpbnd1a  27325  pntpbnd1  27326  pntpbnd2  27327  axlowdimlem16  28483  fzto1st  32533  psgnfzto1st  32535  isarchi3  32604  ofldchr  32703  smatrcl  33075  esumfzf  33366  esumpcvgval  33375  esumcvg  33383  dstfrvunirn  33772  dstfrvclim1  33775  subfacp1lem1  34469  subfacp1lem5  34474  subfaclim  34478  poimirlem7  36799  poimirlem15  36807  poimirlem17  36809  poimirlem19  36811  poimirlem28  36820  lcmineqlem11  41211  lcmineqlem18  41218  lcmineqlem19  41219  lcmineqlem20  41220  4rexfrabdioph  41839  6rexfrabdioph  41840  pellfundge  41923  pellfundgt1  41924  limsup10exlem  44787  wallispilem5  45084  wallispi2lem1  45086  wallispi2  45088  fourierdlem47  45168  nnfoctbdjlem  45470  hoidmvlelem2  45611  vonioolem2  45696  vonicclem2  45699  fmtnof1  46502  lighneallem4b  46576  proththdlem  46580  perfectALTVlem1  46688  perfectALTVlem2  46689  blennngt2o2  47366