Theorem 1e0p1 12816

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 12418	. 2 ⊢ (0 + 1) = 1
2	1	eqcomi 2769	1 ⊢ 1 = (0 + 1)

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7409  0cc0 11157  1c1 11158   + caddc 11160

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-pow 5327  ax-pr 5391  ax-un 7735  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233

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-nel 3062  df-ral 3077  df-rex 3087  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-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-po 5556  df-so 5557  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-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-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-ltxr 11305

This theorem is used by:  6p5e11  12847  7p4e11  12850  8p3e11  12855  9p2e11  12861  fz1ssfz0  13711  fz0to3un2pr  13717  fzo01  13836  fz01pr  13840  bcp1nk  14414  pfx1  14805  arisum2  15983  ege2le3  16209  ef4p  16234  efgt1p2  16235  efgt1p  16236  bitsmod  16559  prmdiv  16909  prmreclem2  17042  vdwap1  17102  11prm  17240  631prm  17252  mulgnn0p1  19242  gsummptfzsplitl  20094  itgcnlem  26057  dveflem  26246  ply1rem  26431  vieta1lem2  26583  vieta1  26584  pserdvlem2  26704  pserdv2  26706  abelthlem6  26712  abelthlem9  26716  cosne0  26806  logf1o2  26927  logtayl  26937  ang180lem3  27088  birthdaylem2  27229  ftalem5  27353  ppi2  27446  ppiublem2  27479  ppiub  27480  bclbnd  27556  bposlem2  27561  lgsdir2lem3  27603  lgseisenlem1  27651  axlowdimlem13  29451  spthispth  30228  uhgrwkspthlem2  30259  cyclnumvtx  30307  upgr3v3e3cycl  30700  upgr4cycl4dv4e  30705  ballotlemii  35056  ballotlem1c  35060  subfacval2  35867  cvmliftlem5  35969  aks6d1c5lem1  43100  sticksstones11  43120  sticksstones12  43122  3cubeslem1  43627  halffl  46227  sinaover2ne0  46794  stoweidlem11  46937  stoweidlem13  46939  stirlinglem7  47006  fourierdlem48  47080  fourierdlem49  47081  fourierdlem69  47101  fourierdlem79  47111  fourierdlem93  47125  etransclem7  47167  etransclem25  47185  etransclem26  47186  etransclem37  47197  iccpartlt  48422  31prm  48598  gpgprismgr4cycllem3  49111  1odd  49184  itcoval1  49691  ackval1  49709  ackval41a  49722