Theorem 1e0p1 12742

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

Syntax hints:   = wceq 1539  (class class class)co 7399  0cc0 11121  1c1 11122   + caddc 11124

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 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197

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-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-po 5558  df-so 5559  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7402  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11263  df-mnf 11264  df-ltxr 11266

This theorem is referenced by:  6p5e11  12773  7p4e11  12776  8p3e11  12781  9p2e11  12787  fz1ssfz0  13629  fz0to3un2pr  13635  fzo01  13752  fz01pr  13756  bcp1nk  14323  pfx1  14708  arisum2  15864  ege2le3  16093  ef4p  16116  efgt1p2  16117  efgt1p  16118  bitsmod  16440  prmdiv  16789  prmreclem2  16922  vdwap1  16982  11prm  17119  631prm  17131  mulgnn0p1  19053  gsummptfzsplitl  19899  itgcnlem  25728  dveflem  25920  ply1rem  26108  vieta1lem2  26256  vieta1  26257  pserdvlem2  26375  pserdv2  26377  abelthlem6  26383  abelthlem9  26387  cosne0  26474  logf1o2  26595  logtayl  26605  ang180lem3  26757  birthdaylem2  26898  ftalem5  27023  ppi2  27116  ppiublem2  27150  ppiub  27151  bclbnd  27227  bposlem2  27232  lgsdir2lem3  27274  lgseisenlem1  27322  axlowdimlem13  28865  spthispth  29638  uhgrwkspthlem2  29668  cyclnumvtx  29714  upgr3v3e3cycl  30093  upgr4cycl4dv4e  30098  ballotlemii  34444  ballotlem1c  34448  subfacval2  35130  cvmliftlem5  35232  aks6d1c5lem1  42071  sticksstones11  42091  sticksstones12  42093  metakunt24  42163  3cubeslem1  42632  halffl  45252  sinaover2ne0  45827  stoweidlem11  45970  stoweidlem13  45972  stirlinglem7  46039  fourierdlem48  46113  fourierdlem49  46114  fourierdlem69  46134  fourierdlem79  46144  fourierdlem93  46158  etransclem7  46200  etransclem25  46218  etransclem26  46219  etransclem37  46230  tworepnotupword  46845  iccpartlt  47356  31prm  47529  1odd  48032  itcoval1  48529  ackval1  48547  ackval41a  48560