Theorem 1e0p1 12861

Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
1e0p1	⊢ 1 = (0 + 1)

Proof of Theorem 1e0p1

Step	Hyp	Ref	Expression
1		0p1e1 12463	. 2 ⊢ (0 + 1) = 1
2	1	eqcomi 2769	1 ⊢ 1 = (0 + 1)

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420  0cc0 11200  1c1 11201   + caddc 11203

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-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

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-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  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-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  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-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-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  6p5e11  12892  7p4e11  12895  8p3e11  12900  9p2e11  12906  fz1ssfz0  13757  fz0to3un2pr  13763  fzo01  13882  fz01pr  13886  bcp1nk  14461  pfx1  14852  arisum2  16030  ege2le3  16256  ef4p  16281  efgt1p2  16282  efgt1p  16283  bitsmod  16606  prmdiv  16962  prmreclem2  17095  vdwap1  17155  11prm  17293  631prm  17305  mulgnn0p1  19295  gsummptfzsplitl  20147  itgcnlem  26110  dveflem  26299  ply1rem  26484  vieta1lem2  26634  vieta1  26635  pserdvlem2  26755  pserdv2  26757  abelthlem6  26763  abelthlem9  26767  cosne0  26857  logf1o2  26978  logtayl  26988  ang180lem3  27139  birthdaylem2  27280  ftalem5  27404  ppi2  27497  ppiublem2  27530  ppiub  27531  bclbnd  27607  bposlem2  27612  lgsdir2lem3  27654  lgseisenlem1  27702  axlowdimlem13  29532  spthispth  30309  uhgrwkspthlem2  30340  cyclnumvtx  30388  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  ballotlemii  35136  ballotlem1c  35140  subfacval2  35952  cvmliftlem5  36054  aks6d1c5lem1  43187  sticksstones11  43207  sticksstones12  43209  3cubeslem1  43695  halffl  46312  sinaover2ne0  46878  stoweidlem11  47021  stoweidlem13  47023  stirlinglem7  47090  fourierdlem48  47164  fourierdlem49  47165  fourierdlem69  47185  fourierdlem79  47195  fourierdlem93  47209  etransclem7  47251  etransclem25  47269  etransclem26  47270  etransclem37  47281  iccpartlt  48506  31prm  48682  gpgprismgr4cycllem3  49195  1odd  49268  itcoval1  49775  ackval1  49793  ackval41a  49806