Theorem 0p1e1 9235

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

Syntax hints:   = wceq 1395  (class class class)co 6007  0cc0 8010  1c1 8011   + caddc 8013

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-addcom 8110  ax-i2m1 8115  ax-0id 8118

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

This theorem is referenced by:  fv0p1e1  9236  zgt0ge1  9516  nn0lt10b  9538  gtndiv  9553  nn0ind-raph  9575  1e0p1  9630  fz01en  10261  fz01or  10319  fz0tp  10330  fz0to3un2pr  10331  elfzonlteqm1  10428  fzo0to2pr  10436  fzo0to3tp  10437  fldiv4p1lem1div2  10537  mulp1mod1  10599  1tonninf  10675  expp1  10780  facp1  10964  faclbnd  10975  bcm1k  10994  bcval5  10997  bcpasc  11000  hash1  11046  binomlem  12010  isumnn0nn  12020  fprodfac  12142  ege2le3  12198  ef4p  12221  eirraplem  12304  p1modz1  12321  nn0o1gt2  12432  bitsfzo  12482  pw2dvdslemn  12703  pcfaclem  12888  4sqlem19  12948  2exp16  12976  ennnfonelemjn  12989  exmidunben  13013  gsumfzconst  13894  gsumfzsnfd  13898  dvply1  15455  lgsne0  15733  gausslemma2dlem4  15759  lgsquadlem2  15773  wlkl1loop  16104  clwwlkccatlem  16143  umgr2cwwk2dif  16166  012of  16444  2o01f  16445  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508