Theorem peano2nnd 12250

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  1c1 11101   + caddc 11103  ℕcn 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-nn 12234

This theorem is referenced by:  bcpasc  14357  relexpsucnnr  15062  o1fsum  15865  bpolydiflem  16108  eftlub  16165  eirrlem  16260  infpnlem1  16970  infpnlem2  16971  prmreclem4  16979  prmreclem5  16980  prmreclem6  16981  vdwlem6  17046  ofldchr  21695  cayhamlem1  22992  ovolunlem1a  25624  ovolicc2lem3  25647  uniioombllem3  25713  uniioombllem4  25714  vieta1lem1  26440  vieta1lem2  26441  aaliou3lem2  26473  lgamgulmlem3  27161  lgamgulmlem4  27162  lgamgulmlem5  27163  lgamgulmlem6  27164  lgamgulm2  27166  lgamcvg2  27185  gamcvg  27186  gamcvg2lem  27189  regamcl  27191  relgamcl  27192  basellem1  27211  basellem2  27212  basellem3  27213  basellem4  27214  basellem5  27215  basellem6  27216  basellem7  27217  basellem8  27218  basellem9  27219  perfectlem1  27359  perfectlem2  27360  bclbnd  27410  lgsdilem2  27463  rplogsumlem2  27615  dchrisumlem2  27620  pntrsumbnd2  27697  pntrlog2bndlem2  27708  pntpbnd1a  27715  pntpbnd1  27716  pntpbnd2  27717  axlowdimlem16  29248  fzto1st  33364  psgnfzto1st  33366  isarchi3  33448  smatrcl  34131  esumfzf  34404  esumpcvgval  34413  esumcvg  34421  dstfrvunirn  34810  dstfrvclim1  34813  subfacp1lem1  35604  subfacp1lem5  35609  subfaclim  35613  poimirlem7  38201  poimirlem15  38209  poimirlem17  38211  poimirlem19  38213  poimirlem28  38222  lcmineqlem11  42731  lcmineqlem18  42738  lcmineqlem19  42739  lcmineqlem20  42740  fimgmcyc  43229  4rexfrabdioph  43452  6rexfrabdioph  43453  pellfundge  43536  pellfundgt1  43537  limsup10exlem  46413  wallispilem5  46710  wallispi2lem1  46712  wallispi2  46714  fourierdlem47  46794  nnfoctbdjlem  47096  hoidmvlelem2  47237  vonioolem2  47322  vonicclem2  47325  fmtnof1  48211  lighneallem4b  48285  proththdlem  48289  perfectALTVlem1  48410  perfectALTVlem2  48411  blennngt2o2  49292