Theorem 0p1e1 9420

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085  0cc0 8179  1c1 8180   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-addcom 8279  ax-i2m1 8284  ax-0id 8287

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  fv0p1e1  9421  zgt0ge1  9707  nn0lt10b  9730  gtndiv  9745  nn0ind-raph  9767  1e0p1  9827  fz01en  10469  fz01or  10528  fz0tp  10539  fz0to3un2pr  10540  elfzonlteqm1  10638  fzo0to2pr  10646  fzo0to3tp  10647  fldiv4p1lem1div2  10753  mulp1mod1  10815  1tonninf  10891  expp1  10996  facp1  11182  faclbnd  11193  bcm1k  11212  bcval5  11215  bcpasc  11218  hash1  11266  binomlem  12266  isumnn0nn  12276  fprodfac  12398  ege2le3  12454  ef4p  12477  eirraplem  12560  p1modz1  12577  nn0o1gt2  12688  bitsfzo  12738  pwbdvdslemn  12960  pcfaclem  13148  4sqlem19  13208  2exp16  13237  37prm  13255  631prm  13261  1259lem3  13264  1259lem4  13265  ennnfonelemjn  13342  exmidunben  13366  gzsumconst  14192  gzsumsnfd  14196  dvply1  15915  efap1p  15929  log2ublem3  16142  bposlem1  16209  lgsne0  16255  gausslemma2dlem4  16281  lgsquadlem2  16295  wlkl1loop  16697  clwwlkccatlem  16739  umgr2cwwk2dif  16763  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  012of  17121  2o01f  17122  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200