Theorem 0p1e1 9368

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 ∈ ℂ
2	1	addlidi 8432	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  9369  zgt0ge1  9653  nn0lt10b  9676  gtndiv  9691  nn0ind-raph  9713  1e0p1  9768  fz01en  10408  fz01or  10467  fz0tp  10478  fz0to3un2pr  10479  elfzonlteqm1  10577  fzo0to2pr  10585  fzo0to3tp  10586  fldiv4p1lem1div2  10689  mulp1mod1  10751  1tonninf  10827  expp1  10932  facp1  11117  faclbnd  11128  bcm1k  11147  bcval5  11150  bcpasc  11153  hash1  11201  binomlem  12194  isumnn0nn  12204  fprodfac  12326  ege2le3  12382  ef4p  12405  eirraplem  12488  p1modz1  12505  nn0o1gt2  12616  bitsfzo  12666  pw2dvdslemn  12887  pcfaclem  13072  4sqlem19  13132  2exp16  13160  ennnfonelemjn  13237  exmidunben  13261  gsumfzconst  14094  gsumfzsnfd  14098  dvply1  15756  lgsne0  16037  gausslemma2dlem4  16063  lgsquadlem2  16077  wlkl1loop  16479  clwwlkccatlem  16521  umgr2cwwk2dif  16545  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  012of  16893  2o01f  16894  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963