Theorem 0p1e1 9419

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 8272	. 2 |- 1 e. CC
2	1	addlidi 8469	1 |- ( 0 + 1 ) = 1

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085   0cc0 8179   1c1 8180   + caddc 8182

This proof depends on 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 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-addcom 8279  ax-i2m1 8284  ax-0id 8287

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

This theorem is used by:  fv0p1e1  9420  zgt0ge1  9705  nn0lt10b  9728  gtndiv  9743  nn0ind-raph  9765  1e0p1  9820  fz01en  10461  fz01or  10520  fz0tp  10531  fz0to3un2pr  10532  elfzonlteqm1  10630  fzo0to2pr  10638  fzo0to3tp  10639  fldiv4p1lem1div2  10742  mulp1mod1  10804  1tonninf  10880  expp1  10985  facp1  11170  faclbnd  11181  bcm1k  11200  bcval5  11203  bcpasc  11206  hash1  11254  binomlem  12252  isumnn0nn  12262  fprodfac  12384  ege2le3  12440  ef4p  12463  eirraplem  12546  p1modz1  12563  nn0o1gt2  12674  bitsfzo  12724  pw2dvdslemn  12945  pcfaclem  13130  4sqlem19  13190  2exp16  13218  ennnfonelemjn  13295  exmidunben  13319  gzsumconst  14145  gzsumsnfd  14149  dvply1  15868  efap1p  15882  log2ublem3  16091  lgsne0  16169  gausslemma2dlem4  16195  lgsquadlem2  16209  wlkl1loop  16611  clwwlkccatlem  16653  umgr2cwwk2dif  16677  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  012of  17035  2o01f  17036  isomninnlem  17091  iswomninnlem  17111  ismkvnnlem  17114