Theorem peano2nnd 12265

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7413  1c1 11138   + caddc 11140  ℕcn 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-nn 12249

This theorem is referenced by:  bcpasc  14342  relexpsucnnr  15046  o1fsum  15831  bpolydiflem  16072  eftlub  16127  eirrlem  16222  infpnlem1  16930  infpnlem2  16931  prmreclem4  16939  prmreclem5  16940  prmreclem6  16941  vdwlem6  17006  cayhamlem1  22820  ovolunlem1a  25467  ovolicc2lem3  25490  uniioombllem3  25556  uniioombllem4  25557  vieta1lem1  26288  vieta1lem2  26289  aaliou3lem2  26321  lgamgulmlem3  27010  lgamgulmlem4  27011  lgamgulmlem5  27012  lgamgulmlem6  27013  lgamgulm2  27015  lgamcvg2  27034  gamcvg  27035  gamcvg2lem  27038  regamcl  27040  relgamcl  27041  basellem1  27060  basellem2  27061  basellem3  27062  basellem4  27063  basellem5  27064  basellem6  27065  basellem7  27066  basellem8  27067  basellem9  27068  perfectlem1  27209  perfectlem2  27210  bclbnd  27260  lgsdilem2  27313  rplogsumlem2  27465  dchrisumlem2  27470  pntrsumbnd2  27547  pntrlog2bndlem2  27558  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  axlowdimlem16  28902  fzto1st  33062  psgnfzto1st  33064  isarchi3  33133  ofldchr  33284  smatrcl  33754  esumfzf  34029  esumpcvgval  34038  esumcvg  34046  dstfrvunirn  34436  dstfrvclim1  34439  subfacp1lem1  35143  subfacp1lem5  35148  subfaclim  35152  poimirlem7  37593  poimirlem15  37601  poimirlem17  37603  poimirlem19  37605  poimirlem28  37614  lcmineqlem11  41999  lcmineqlem18  42006  lcmineqlem19  42007  lcmineqlem20  42008  fimgmcyc  42507  4rexfrabdioph  42772  6rexfrabdioph  42773  pellfundge  42856  pellfundgt1  42857  limsup10exlem  45744  wallispilem5  46041  wallispi2lem1  46043  wallispi2  46045  fourierdlem47  46125  nnfoctbdjlem  46427  hoidmvlelem2  46568  vonioolem2  46653  vonicclem2  46656  fmtnof1  47480  lighneallem4b  47554  proththdlem  47558  perfectALTVlem1  47666  perfectALTVlem2  47667  blennngt2o2  48471