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 ∈ ℂ
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  12062  isumnn0nn  12072  fprodfac  12194  ege2le3  12250  ef4p  12273  eirraplem  12356  p1modz1  12373  nn0o1gt2  12484  bitsfzo  12534  pw2dvdslemn  12755  pcfaclem  12940  4sqlem19  13000  2exp16  13028  ennnfonelemjn  13041  exmidunben  13065  gsumfzconst  13946  gsumfzsnfd  13950  dvply1  15508  lgsne0  15786  gausslemma2dlem4  15812  lgsquadlem2  15826  wlkl1loop  16228  clwwlkccatlem  16270  umgr2cwwk2dif  16294  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  012of  16643  2o01f  16644  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708