Theorem 1e0p1 12786

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416  0cc0 11127  1c1 11128   + caddc 11130

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is used by:  6p5e11  12817  7p4e11  12820  8p3e11  12825  9p2e11  12831  fz1ssfz0  13680  fz0to3un2pr  13686  fzo01  13805  fz01pr  13809  bcp1nk  14383  pfx1  14774  arisum2  15952  ege2le3  16180  ef4p  16205  efgt1p2  16206  efgt1p  16207  bitsmod  16530  prmdiv  16880  prmreclem2  17013  vdwap1  17073  11prm  17211  631prm  17223  mulgnn0p1  19209  gsummptfzsplitl  20061  itgcnlem  26019  dveflem  26208  ply1rem  26393  vieta1lem2  26542  vieta1  26543  pserdvlem2  26661  pserdv2  26663  abelthlem6  26669  abelthlem9  26673  cosne0  26764  logf1o2  26885  logtayl  26895  ang180lem3  27046  birthdaylem2  27187  ftalem5  27311  ppi2  27404  ppiublem2  27437  ppiub  27438  bclbnd  27514  bposlem2  27519  lgsdir2lem3  27561  lgseisenlem1  27609  axlowdimlem13  29397  spthispth  30174  uhgrwkspthlem2  30205  cyclnumvtx  30253  upgr3v3e3cycl  30646  upgr4cycl4dv4e  30651  ballotlemii  35002  ballotlem1c  35006  subfacval2  35753  cvmliftlem5  35855  aks6d1c5lem1  42989  sticksstones11  43009  sticksstones12  43011  3cubeslem1  43516  halffl  46116  sinaover2ne0  46683  stoweidlem11  46826  stoweidlem13  46828  stirlinglem7  46895  fourierdlem48  46969  fourierdlem49  46970  fourierdlem69  46990  fourierdlem79  47000  fourierdlem93  47014  etransclem7  47056  etransclem25  47074  etransclem26  47075  etransclem37  47086  iccpartlt  48311  31prm  48487  gpgprismgr4cycllem3  49000  1odd  49073  itcoval1  49580  ackval1  49598  ackval41a  49611