Theorem 0p1e1 9371

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

Syntax hints:   = wceq 1398  (class class class)co 6058   0cc0 8143   1c1 8144   + caddc 8146

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 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  fv0p1e1  9372  zgt0ge1  9656  nn0lt10b  9679  gtndiv  9694  nn0ind-raph  9716  1e0p1  9771  fz01en  10411  fz01or  10470  fz0tp  10481  fz0to3un2pr  10482  elfzonlteqm1  10580  fzo0to2pr  10588  fzo0to3tp  10589  fldiv4p1lem1div2  10692  mulp1mod1  10754  1tonninf  10830  expp1  10935  facp1  11120  faclbnd  11131  bcm1k  11150  bcval5  11153  bcpasc  11156  hash1  11204  binomlem  12197  isumnn0nn  12207  fprodfac  12329  ege2le3  12385  ef4p  12408  eirraplem  12491  p1modz1  12508  nn0o1gt2  12619  bitsfzo  12669  pw2dvdslemn  12890  pcfaclem  13075  4sqlem19  13135  2exp16  13163  ennnfonelemjn  13240  exmidunben  13264  gsumfzconst  14097  gsumfzsnfd  14101  dvply1  15759  lgsne0  16040  gausslemma2dlem4  16066  lgsquadlem2  16080  wlkl1loop  16482  clwwlkccatlem  16524  umgr2cwwk2dif  16548  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  012of  16906  2o01f  16907  isomninnlem  16953  iswomninnlem  16973  ismkvnnlem  16976