Theorem 0p1e1 9351

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 8220	. 2 ⊢ 1 ∈ ℂ
2	1	addlidi 8416	1 ⊢ (0 + 1) = 1

Syntax hints:   = wceq 1398  (class class class)co 6050  0cc0 8127  1c1 8128   + caddc 8130

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 2214  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-addcom 8227  ax-i2m1 8232  ax-0id 8235

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  fv0p1e1  9352  zgt0ge1  9636  nn0lt10b  9658  gtndiv  9673  nn0ind-raph  9695  1e0p1  9750  fz01en  10387  fz01or  10445  fz0tp  10456  fz0to3un2pr  10457  elfzonlteqm1  10555  fzo0to2pr  10563  fzo0to3tp  10564  fldiv4p1lem1div2  10665  mulp1mod1  10727  1tonninf  10803  expp1  10908  facp1  11092  faclbnd  11103  bcm1k  11122  bcval5  11125  bcpasc  11128  hash1  11176  binomlem  12169  isumnn0nn  12179  fprodfac  12301  ege2le3  12357  ef4p  12380  eirraplem  12463  p1modz1  12480  nn0o1gt2  12591  bitsfzo  12641  pw2dvdslemn  12862  pcfaclem  13047  4sqlem19  13107  2exp16  13135  ennnfonelemjn  13153  exmidunben  13177  gsumfzconst  14058  gsumfzsnfd  14062  dvply1  15630  lgsne0  15911  gausslemma2dlem4  15937  lgsquadlem2  15951  wlkl1loop  16353  clwwlkccatlem  16395  umgr2cwwk2dif  16419  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  012of  16767  2o01f  16768  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837