Theorem 0p1e1 9262

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

Syntax hints:   = wceq 1397  (class class class)co 6023   0cc0 8037   1c1 8038   + caddc 8040

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2212  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-addcom 8137  ax-i2m1 8142  ax-0id 8145

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226

This theorem is referenced by:  fv0p1e1  9263  zgt0ge1  9543  nn0lt10b  9565  gtndiv  9580  nn0ind-raph  9602  1e0p1  9657  fz01en  10293  fz01or  10351  fz0tp  10362  fz0to3un2pr  10363  elfzonlteqm1  10461  fzo0to2pr  10469  fzo0to3tp  10470  fldiv4p1lem1div2  10571  mulp1mod1  10633  1tonninf  10709  expp1  10814  facp1  10998  faclbnd  11009  bcm1k  11028  bcval5  11031  bcpasc  11034  hash1  11081  binomlem  12067  isumnn0nn  12077  fprodfac  12199  ege2le3  12255  ef4p  12278  eirraplem  12361  p1modz1  12378  nn0o1gt2  12489  bitsfzo  12539  pw2dvdslemn  12760  pcfaclem  12945  4sqlem19  13005  2exp16  13033  ennnfonelemjn  13046  exmidunben  13070  gsumfzconst  13951  gsumfzsnfd  13955  dvply1  15518  lgsne0  15796  gausslemma2dlem4  15822  lgsquadlem2  15836  wlkl1loop  16238  clwwlkccatlem  16280  umgr2cwwk2dif  16304  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  012of  16652  2o01f  16653  isomninnlem  16701  iswomninnlem  16721  ismkvnnlem  16724