Theorem 0p1e1 9257

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

Syntax hints:   = wceq 1397  (class class class)co 6018   0cc0 8032   1c1 8033   + caddc 8035

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 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-addcom 8132  ax-i2m1 8137  ax-0id 8140

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

This theorem is referenced by:  fv0p1e1  9258  zgt0ge1  9538  nn0lt10b  9560  gtndiv  9575  nn0ind-raph  9597  1e0p1  9652  fz01en  10288  fz01or  10346  fz0tp  10357  fz0to3un2pr  10358  elfzonlteqm1  10456  fzo0to2pr  10464  fzo0to3tp  10465  fldiv4p1lem1div2  10566  mulp1mod1  10628  1tonninf  10704  expp1  10809  facp1  10993  faclbnd  11004  bcm1k  11023  bcval5  11026  bcpasc  11029  hash1  11076  binomlem  12046  isumnn0nn  12056  fprodfac  12178  ege2le3  12234  ef4p  12257  eirraplem  12340  p1modz1  12357  nn0o1gt2  12468  bitsfzo  12518  pw2dvdslemn  12739  pcfaclem  12924  4sqlem19  12984  2exp16  13012  ennnfonelemjn  13025  exmidunben  13049  gsumfzconst  13930  gsumfzsnfd  13934  dvply1  15492  lgsne0  15770  gausslemma2dlem4  15796  lgsquadlem2  15810  wlkl1loop  16212  clwwlkccatlem  16254  umgr2cwwk2dif  16278  012of  16613  2o01f  16614  isomninnlem  16655  iswomninnlem  16674  ismkvnnlem  16677