Theorem 0p1e1 9401

Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
0p1e1	|- ( 0 + 1 ) = 1

Proof of Theorem 0p1e1

Step	Hyp	Ref	Expression
1		ax-1cn 8266	. 2 |- 1 e. CC
2	1	addlidi 8463	1 |- ( 0 + 1 ) = 1

Syntax hints:   = wceq 1402  (class class class)co 6079   0cc0 8173   1c1 8174   + caddc 8176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8266  ax-icn 8268  ax-addcl 8269  ax-mulcl 8271  ax-addcom 8273  ax-i2m1 8278  ax-0id 8281

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  fv0p1e1  9402  zgt0ge1  9686  nn0lt10b  9709  gtndiv  9724  nn0ind-raph  9746  1e0p1  9801  fz01en  10442  fz01or  10501  fz0tp  10512  fz0to3un2pr  10513  elfzonlteqm1  10611  fzo0to2pr  10619  fzo0to3tp  10620  fldiv4p1lem1div2  10723  mulp1mod1  10785  1tonninf  10861  expp1  10966  facp1  11151  faclbnd  11162  bcm1k  11181  bcval5  11184  bcpasc  11187  hash1  11235  binomlem  12233  isumnn0nn  12243  fprodfac  12365  ege2le3  12421  ef4p  12444  eirraplem  12527  p1modz1  12544  nn0o1gt2  12655  bitsfzo  12705  pw2dvdslemn  12926  pcfaclem  13111  4sqlem19  13171  2exp16  13199  ennnfonelemjn  13276  exmidunben  13300  gzsumconst  14126  gzsumsnfd  14130  dvply1  15849  log2ublem3  16068  lgsne0  16140  gausslemma2dlem4  16166  lgsquadlem2  16180  wlkl1loop  16582  clwwlkccatlem  16624  umgr2cwwk2dif  16648  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  012of  17006  2o01f  17007  isomninnlem  17053  iswomninnlem  17073  ismkvnnlem  17076