Theorem peano2nnd 12352

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  1c1 11201   + caddc 11203  ℕcn 12335

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-nn 12336

This theorem is used by:  bcpasc  14465  relexpsucnnr  15178  o1fsum  15980  bpolydiflem  16220  eftlub  16277  eirrlem  16372  infpnlem1  17088  infpnlem2  17089  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  vdwlem6  17164  ofldchr  21882  cayhamlem1  23184  ovolunlem1a  25817  ovolicc2lem3  25840  uniioombllem3  25906  uniioombllem4  25907  vieta1lem1  26633  vieta1lem2  26634  aaliou3lem2  26670  lgamgulmlem3  27358  lgamgulmlem4  27359  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  regamcl  27388  relgamcl  27389  basellem1  27408  basellem2  27409  basellem3  27410  basellem4  27411  basellem5  27412  basellem6  27413  basellem7  27414  basellem8  27415  basellem9  27416  perfectlem1  27556  perfectlem2  27557  bclbnd  27607  lgsdilem2  27660  rplogsumlem2  27812  dchrisumlem2  27817  pntrsumbnd2  27894  pntrlog2bndlem2  27905  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  axlowdimlem16  29535  fzto1st  33664  psgnfzto1st  33666  isarchi3  33748  smatrcl  34428  esumfzf  34701  esumpcvgval  34710  esumcvg  34718  dstfrvunirn  35107  dstfrvclim1  35110  subfacp1lem1  35944  subfacp1lem5  35949  subfaclim  35953  poimirlem7  38546  poimirlem15  38554  poimirlem17  38556  poimirlem19  38558  poimirlem28  38567  lcmineqlem11  43090  lcmineqlem18  43097  lcmineqlem19  43098  lcmineqlem20  43099  fimgmcyc  43599  4rexfrabdioph  43805  6rexfrabdioph  43806  pellfundge  43889  pellfundgt1  43890  limsup10exlem  46782  wallispilem5  47079  wallispi2lem1  47081  wallispi2  47083  fourierdlem47  47163  nnfoctbdjlem  47465  hoidmvlelem2  47606  vonioolem2  47691  vonicclem2  47694  fmtnof1  48620  lighneallem4b  48694  proththdlem  48698  perfectALTVlem1  48819  perfectALTVlem2  48820  blennngt2o2  49704