Theorem 0p1e1 9256

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

Syntax hints:   = wceq 1397  (class class class)co 6017  0cc0 8031  1c1 8032   + caddc 8034

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-addcom 8131  ax-i2m1 8136  ax-0id 8139

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  fv0p1e1  9257  zgt0ge1  9537  nn0lt10b  9559  gtndiv  9574  nn0ind-raph  9596  1e0p1  9651  fz01en  10287  fz01or  10345  fz0tp  10356  fz0to3un2pr  10357  elfzonlteqm1  10454  fzo0to2pr  10462  fzo0to3tp  10463  fldiv4p1lem1div2  10564  mulp1mod1  10626  1tonninf  10702  expp1  10807  facp1  10991  faclbnd  11002  bcm1k  11021  bcval5  11024  bcpasc  11027  hash1  11074  binomlem  12043  isumnn0nn  12053  fprodfac  12175  ege2le3  12231  ef4p  12254  eirraplem  12337  p1modz1  12354  nn0o1gt2  12465  bitsfzo  12515  pw2dvdslemn  12736  pcfaclem  12921  4sqlem19  12981  2exp16  13009  ennnfonelemjn  13022  exmidunben  13046  gsumfzconst  13927  gsumfzsnfd  13931  dvply1  15488  lgsne0  15766  gausslemma2dlem4  15792  lgsquadlem2  15806  wlkl1loop  16208  clwwlkccatlem  16250  umgr2cwwk2dif  16274  012of  16592  2o01f  16593  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656