Theorem peano2nnd 12229

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  1c1 11076   + caddc 11078  ℕcn 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-nn 12213

This theorem is referenced by:  bcpasc  14336  relexpsucnnr  15040  o1fsum  15843  bpolydiflem  16086  eftlub  16143  eirrlem  16238  infpnlem1  16948  infpnlem2  16949  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  vdwlem6  17024  ofldchr  21630  cayhamlem1  22928  ovolunlem1a  25560  ovolicc2lem3  25583  uniioombllem3  25649  uniioombllem4  25650  vieta1lem1  26376  vieta1lem2  26377  aaliou3lem2  26409  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem5  27099  lgamgulmlem6  27100  lgamgulm2  27102  lgamcvg2  27121  gamcvg  27122  gamcvg2lem  27125  regamcl  27127  relgamcl  27128  basellem1  27147  basellem2  27148  basellem3  27149  basellem4  27150  basellem5  27151  basellem6  27152  basellem7  27153  basellem8  27154  basellem9  27155  perfectlem1  27295  perfectlem2  27296  bclbnd  27346  lgsdilem2  27399  rplogsumlem2  27551  dchrisumlem2  27556  pntrsumbnd2  27633  pntrlog2bndlem2  27644  pntpbnd1a  27651  pntpbnd1  27652  pntpbnd2  27653  axlowdimlem16  29160  fzto1st  33285  psgnfzto1st  33287  isarchi3  33369  smatrcl  34095  esumfzf  34368  esumpcvgval  34377  esumcvg  34385  dstfrvunirn  34774  dstfrvclim1  34777  subfacp1lem1  35534  subfacp1lem5  35539  subfaclim  35543  poimirlem7  38131  poimirlem15  38139  poimirlem17  38141  poimirlem19  38143  poimirlem28  38152  lcmineqlem11  42661  lcmineqlem18  42668  lcmineqlem19  42669  lcmineqlem20  42670  fimgmcyc  43157  4rexfrabdioph  43380  6rexfrabdioph  43381  pellfundge  43464  pellfundgt1  43465  limsup10exlem  46351  wallispilem5  46648  wallispi2lem1  46650  wallispi2  46652  fourierdlem47  46732  nnfoctbdjlem  47034  hoidmvlelem2  47175  vonioolem2  47260  vonicclem2  47263  fmtnof1  48149  lighneallem4b  48223  proththdlem  48227  perfectALTVlem1  48348  perfectALTVlem2  48349  blennngt2o2  49219