Theorem peano2nnd 12179

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  1c1 11045   + caddc 11047  ℕcn 12162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163

This theorem is referenced by:  bcpasc  14262  relexpsucnnr  14967  o1fsum  15755  bpolydiflem  15996  eftlub  16053  eirrlem  16148  infpnlem1  16857  infpnlem2  16858  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  vdwlem6  16933  ofldchr  21518  cayhamlem1  22786  ovolunlem1a  25430  ovolicc2lem3  25453  uniioombllem3  25519  uniioombllem4  25520  vieta1lem1  26251  vieta1lem2  26252  aaliou3lem2  26284  lgamgulmlem3  26974  lgamgulmlem4  26975  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgamcvg2  26998  gamcvg  26999  gamcvg2lem  27002  regamcl  27004  relgamcl  27005  basellem1  27024  basellem2  27025  basellem3  27026  basellem4  27027  basellem5  27028  basellem6  27029  basellem7  27030  basellem8  27031  basellem9  27032  perfectlem1  27173  perfectlem2  27174  bclbnd  27224  lgsdilem2  27277  rplogsumlem2  27429  dchrisumlem2  27434  pntrsumbnd2  27511  pntrlog2bndlem2  27522  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  axlowdimlem16  28937  fzto1st  33075  psgnfzto1st  33077  isarchi3  33156  smatrcl  33779  esumfzf  34052  esumpcvgval  34061  esumcvg  34069  dstfrvunirn  34459  dstfrvclim1  34462  subfacp1lem1  35159  subfacp1lem5  35164  subfaclim  35168  poimirlem7  37614  poimirlem15  37622  poimirlem17  37624  poimirlem19  37626  poimirlem28  37635  lcmineqlem11  42020  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem20  42029  fimgmcyc  42515  4rexfrabdioph  42779  6rexfrabdioph  42780  pellfundge  42863  pellfundgt1  42864  limsup10exlem  45763  wallispilem5  46060  wallispi2lem1  46062  wallispi2  46064  fourierdlem47  46144  nnfoctbdjlem  46446  hoidmvlelem2  46587  vonioolem2  46672  vonicclem2  46675  fmtnof1  47529  lighneallem4b  47603  proththdlem  47607  perfectALTVlem1  47715  perfectALTVlem2  47716  blennngt2o2  48574