Theorem peano2nnd 12186

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7362  1c1 11034   + caddc 11036  ℕcn 12169

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-om 7813  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-nn 12170

This theorem is referenced by:  bcpasc  14278  relexpsucnnr  14982  o1fsum  15771  bpolydiflem  16014  eftlub  16071  eirrlem  16166  infpnlem1  16876  infpnlem2  16877  prmreclem4  16885  prmreclem5  16886  prmreclem6  16887  vdwlem6  16952  ofldchr  21570  cayhamlem1  22845  ovolunlem1a  25477  ovolicc2lem3  25500  uniioombllem3  25566  uniioombllem4  25567  vieta1lem1  26291  vieta1lem2  26292  aaliou3lem2  26324  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  regamcl  27042  relgamcl  27043  basellem1  27062  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  basellem6  27067  basellem7  27068  basellem8  27069  basellem9  27070  perfectlem1  27210  perfectlem2  27211  bclbnd  27261  lgsdilem2  27314  rplogsumlem2  27466  dchrisumlem2  27471  pntrsumbnd2  27548  pntrlog2bndlem2  27559  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  axlowdimlem16  29044  fzto1st  33183  psgnfzto1st  33185  isarchi3  33267  smatrcl  33960  esumfzf  34233  esumpcvgval  34242  esumcvg  34250  dstfrvunirn  34639  dstfrvclim1  34642  subfacp1lem1  35381  subfacp1lem5  35386  subfaclim  35390  poimirlem7  37968  poimirlem15  37976  poimirlem17  37978  poimirlem19  37980  poimirlem28  37989  lcmineqlem11  42498  lcmineqlem18  42505  lcmineqlem19  42506  lcmineqlem20  42507  fimgmcyc  42999  4rexfrabdioph  43250  6rexfrabdioph  43251  pellfundge  43334  pellfundgt1  43335  limsup10exlem  46224  wallispilem5  46521  wallispi2lem1  46523  wallispi2  46525  fourierdlem47  46605  nnfoctbdjlem  46907  hoidmvlelem2  47048  vonioolem2  47133  vonicclem2  47136  fmtnof1  48016  lighneallem4b  48090  proththdlem  48094  perfectALTVlem1  48215  perfectALTVlem2  48216  blennngt2o2  49086