Theorem 0p1e1 9373

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

Syntax hints:   = wceq 1398  (class class class)co 6060   0cc0 8145   1c1 8146   + caddc 8148

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 8238  ax-icn 8240  ax-addcl 8241  ax-mulcl 8243  ax-addcom 8245  ax-i2m1 8250  ax-0id 8253

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

This theorem is referenced by:  fv0p1e1  9374  zgt0ge1  9658  nn0lt10b  9681  gtndiv  9696  nn0ind-raph  9718  1e0p1  9773  fz01en  10413  fz01or  10472  fz0tp  10483  fz0to3un2pr  10484  elfzonlteqm1  10582  fzo0to2pr  10590  fzo0to3tp  10591  fldiv4p1lem1div2  10694  mulp1mod1  10756  1tonninf  10832  expp1  10937  facp1  11122  faclbnd  11133  bcm1k  11152  bcval5  11155  bcpasc  11158  hash1  11206  binomlem  12200  isumnn0nn  12210  fprodfac  12332  ege2le3  12388  ef4p  12411  eirraplem  12494  p1modz1  12511  nn0o1gt2  12622  bitsfzo  12672  pw2dvdslemn  12893  pcfaclem  13078  4sqlem19  13138  2exp16  13166  ennnfonelemjn  13243  exmidunben  13267  gsumfzconst  14100  gsumfzsnfd  14104  dvply1  15762  lgsne0  16043  gausslemma2dlem4  16069  lgsquadlem2  16083  wlkl1loop  16485  clwwlkccatlem  16527  umgr2cwwk2dif  16551  konigsberglem1  16615  konigsberglem2  16616  konigsberglem3  16617  012of  16909  2o01f  16910  isomninnlem  16956  iswomninnlem  16976  ismkvnnlem  16979