Theorem peano2nnd 10914

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  1c1 9816   + caddc 9818  ℕcn 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898

This theorem is referenced by:  bcpasc  12970  relexpsucnnr  13613  o1fsum  14386  bpolydiflem  14624  eftlub  14678  eirrlem  14771  infpnlem1  15452  infpnlem2  15453  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  vdwlem6  15528  cayhamlem1  20490  ovolunlem1a  23071  ovolicc2lem3  23094  uniioombllem3  23159  uniioombllem4  23160  vieta1lem1  23869  vieta1lem2  23870  aaliou3lem2  23902  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  regamcl  24587  relgamcl  24588  basellem1  24607  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  perfectlem1  24754  perfectlem2  24755  bclbnd  24805  lgsdilem2  24858  rplogsumlem2  24974  dchrisumlem2  24979  pntrsumbnd2  25056  pntrlog2bndlem2  25067  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  axlowdimlem16  25637  isarchi3  29072  ofldchr  29145  fzto1st  29184  psgnfzto1st  29186  smatrcl  29190  esumfzf  29458  esumpcvgval  29467  esumcvg  29475  dstfrvunirn  29863  dstfrvclim1  29866  subfacp1lem1  30415  subfacp1lem5  30420  subfaclim  30424  poimirlem7  32586  poimirlem15  32594  poimirlem17  32596  poimirlem19  32598  poimirlem28  32607  4rexfrabdioph  36380  6rexfrabdioph  36381  pellfundge  36464  pellfundgt1  36465  wallispilem5  38962  wallispi2lem1  38964  wallispi2  38966  fourierdlem47  39046  nnfoctbdjlem  39348  hoidmvlelem2  39486  vonioolem2  39572  vonicclem2  39575  fmtnof1  39985  fmtnoprmfac1lem  40014  lighneallem4b  40064  proththdlem  40068  perfectALTVlem1  40164  perfectALTVlem2  40165  blennngt2o2  42184