Theorem 1e0p1 12683

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

Syntax hints:   = wceq 1542  (class class class)co 7364  0cc0 11035  1c1 11036   + caddc 11038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-po 5536  df-so 5537  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7367  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181

This theorem is referenced by:  6p5e11  12714  7p4e11  12717  8p3e11  12722  9p2e11  12728  fz1ssfz0  13574  fz0to3un2pr  13580  fzo01  13699  fz01pr  13703  bcp1nk  14276  pfx1  14662  arisum2  15823  ege2le3  16052  ef4p  16077  efgt1p2  16078  efgt1p  16079  bitsmod  16402  prmdiv  16752  prmreclem2  16885  vdwap1  16945  11prm  17082  631prm  17094  mulgnn0p1  19058  gsummptfzsplitl  19905  itgcnlem  25773  dveflem  25962  ply1rem  26147  vieta1lem2  26294  vieta1  26295  pserdvlem2  26412  pserdv2  26414  abelthlem6  26420  abelthlem9  26424  cosne0  26512  logf1o2  26633  logtayl  26643  ang180lem3  26794  birthdaylem2  26935  ftalem5  27060  ppi2  27153  ppiublem2  27186  ppiub  27187  bclbnd  27263  bposlem2  27268  lgsdir2lem3  27310  lgseisenlem1  27358  axlowdimlem13  29043  spthispth  29813  uhgrwkspthlem2  29843  cyclnumvtx  29889  upgr3v3e3cycl  30271  upgr4cycl4dv4e  30276  ballotlemii  34670  ballotlem1c  34674  subfacval2  35391  cvmliftlem5  35493  aks6d1c5lem1  42597  sticksstones11  42617  sticksstones12  42619  3cubeslem1  43138  halffl  45755  sinaover2ne0  46322  stoweidlem11  46465  stoweidlem13  46467  stirlinglem7  46534  fourierdlem48  46608  fourierdlem49  46609  fourierdlem69  46629  fourierdlem79  46639  fourierdlem93  46653  etransclem7  46695  etransclem25  46713  etransclem26  46714  etransclem37  46725  iccpartlt  47904  31prm  48080  gpgprismgr4cycllem3  48593  1odd  48667  itcoval1  49159  ackval1  49177  ackval41a  49190