Theorem peano2nnd 12307

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7409  1c1 11158   + caddc 11160  ℕcn 12290

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-om 7862  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-nn 12291

This theorem is used by:  bcpasc  14418  relexpsucnnr  15131  o1fsum  15933  bpolydiflem  16173  eftlub  16230  eirrlem  16325  infpnlem1  17035  infpnlem2  17036  prmreclem4  17044  prmreclem5  17045  prmreclem6  17046  vdwlem6  17111  ofldchr  21829  cayhamlem1  23131  ovolunlem1a  25764  ovolicc2lem3  25787  uniioombllem3  25853  uniioombllem4  25854  vieta1lem1  26582  vieta1lem2  26583  aaliou3lem2  26619  lgamgulmlem3  27307  lgamgulmlem4  27308  lgamgulmlem5  27309  lgamgulmlem6  27310  lgamgulm2  27312  lgamcvg2  27331  gamcvg  27332  gamcvg2lem  27335  regamcl  27337  relgamcl  27338  basellem1  27357  basellem2  27358  basellem3  27359  basellem4  27360  basellem5  27361  basellem6  27362  basellem7  27363  basellem8  27364  basellem9  27365  perfectlem1  27505  perfectlem2  27506  bclbnd  27556  lgsdilem2  27609  rplogsumlem2  27761  dchrisumlem2  27766  pntrsumbnd2  27843  pntrlog2bndlem2  27854  pntpbnd1a  27861  pntpbnd1  27862  pntpbnd2  27863  axlowdimlem16  29454  fzto1st  33583  psgnfzto1st  33585  isarchi3  33667  smatrcl  34347  esumfzf  34620  esumpcvgval  34629  esumcvg  34637  dstfrvunirn  35027  dstfrvclim1  35030  subfacp1lem1  35859  subfacp1lem5  35864  subfaclim  35868  poimirlem7  38459  poimirlem15  38467  poimirlem17  38469  poimirlem19  38471  poimirlem28  38480  lcmineqlem11  43003  lcmineqlem18  43010  lcmineqlem19  43011  lcmineqlem20  43012  fimgmcyc  43514  4rexfrabdioph  43737  6rexfrabdioph  43738  pellfundge  43821  pellfundgt1  43822  limsup10exlem  46698  wallispilem5  46995  wallispi2lem1  46997  wallispi2  46999  fourierdlem47  47079  nnfoctbdjlem  47381  hoidmvlelem2  47522  vonioolem2  47607  vonicclem2  47610  fmtnof1  48536  lighneallem4b  48610  proththdlem  48614  perfectALTVlem1  48735  perfectALTVlem2  48736  blennngt2o2  49620