Theorem 0p1e1 9224

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

Syntax hints:   = wceq 1395  (class class class)co 6001  0cc0 7999  1c1 8000   + caddc 8002

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 8092  ax-icn 8094  ax-addcl 8095  ax-mulcl 8097  ax-addcom 8099  ax-i2m1 8104  ax-0id 8107

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

This theorem is referenced by:  fv0p1e1  9225  zgt0ge1  9505  nn0lt10b  9527  gtndiv  9542  nn0ind-raph  9564  1e0p1  9619  fz01en  10249  fz01or  10307  fz0tp  10318  fz0to3un2pr  10319  elfzonlteqm1  10416  fzo0to2pr  10424  fzo0to3tp  10425  fldiv4p1lem1div2  10525  mulp1mod1  10587  1tonninf  10663  expp1  10768  facp1  10952  faclbnd  10963  bcm1k  10982  bcval5  10985  bcpasc  10988  hash1  11033  binomlem  11994  isumnn0nn  12004  fprodfac  12126  ege2le3  12182  ef4p  12205  eirraplem  12288  p1modz1  12305  nn0o1gt2  12416  bitsfzo  12466  pw2dvdslemn  12687  pcfaclem  12872  4sqlem19  12932  2exp16  12960  ennnfonelemjn  12973  exmidunben  12997  gsumfzconst  13878  gsumfzsnfd  13882  dvply1  15439  lgsne0  15717  gausslemma2dlem4  15743  lgsquadlem2  15757  wlkl1loop  16069  012of  16357  2o01f  16358  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420