Theorem 0p1e1 9347

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

Syntax hints:   = wceq 1398  (class class class)co 6049   0cc0 8123   1c1 8124   + caddc 8126

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-addcom 8223  ax-i2m1 8228  ax-0id 8231

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  fv0p1e1  9348  zgt0ge1  9632  nn0lt10b  9654  gtndiv  9669  nn0ind-raph  9691  1e0p1  9746  fz01en  10383  fz01or  10441  fz0tp  10452  fz0to3un2pr  10453  elfzonlteqm1  10551  fzo0to2pr  10559  fzo0to3tp  10560  fldiv4p1lem1div2  10661  mulp1mod1  10723  1tonninf  10799  expp1  10904  facp1  11088  faclbnd  11099  bcm1k  11118  bcval5  11121  bcpasc  11124  hash1  11171  binomlem  12162  isumnn0nn  12172  fprodfac  12294  ege2le3  12350  ef4p  12373  eirraplem  12456  p1modz1  12473  nn0o1gt2  12584  bitsfzo  12634  pw2dvdslemn  12855  pcfaclem  13040  4sqlem19  13100  2exp16  13128  ennnfonelemjn  13142  exmidunben  13166  gsumfzconst  14047  gsumfzsnfd  14051  dvply1  15617  lgsne0  15898  gausslemma2dlem4  15924  lgsquadlem2  15938  wlkl1loop  16340  clwwlkccatlem  16382  umgr2cwwk2dif  16406  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  012of  16754  2o01f  16755  isomninnlem  16801  iswomninnlem  16821  ismkvnnlem  16824