Theorem 0p1e1 9397

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

Syntax hints:   = wceq 1402  (class class class)co 6075  0cc0 8169  1c1 8170   + caddc 8172

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-addcom 8269  ax-i2m1 8274  ax-0id 8277

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

This theorem is referenced by:  fv0p1e1  9398  zgt0ge1  9682  nn0lt10b  9705  gtndiv  9720  nn0ind-raph  9742  1e0p1  9797  fz01en  10437  fz01or  10496  fz0tp  10507  fz0to3un2pr  10508  elfzonlteqm1  10606  fzo0to2pr  10614  fzo0to3tp  10615  fldiv4p1lem1div2  10718  mulp1mod1  10780  1tonninf  10856  expp1  10961  facp1  11146  faclbnd  11157  bcm1k  11176  bcval5  11179  bcpasc  11182  hash1  11230  binomlem  12228  isumnn0nn  12238  fprodfac  12360  ege2le3  12416  ef4p  12439  eirraplem  12522  p1modz1  12539  nn0o1gt2  12650  bitsfzo  12700  pw2dvdslemn  12921  pcfaclem  13106  4sqlem19  13166  2exp16  13194  ennnfonelemjn  13271  exmidunben  13295  gzsumconst  14120  gzsumsnfd  14124  dvply1  15789  lgsne0  16071  gausslemma2dlem4  16097  lgsquadlem2  16111  wlkl1loop  16513  clwwlkccatlem  16555  umgr2cwwk2dif  16579  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  012of  16937  2o01f  16938  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007