Theorem 0p1e1 9152

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

Syntax hints:   = wceq 1373  (class class class)co 5946  0cc0 7927  1c1 7928   + caddc 7930

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1cn 8020  ax-icn 8022  ax-addcl 8023  ax-mulcl 8025  ax-addcom 8027  ax-i2m1 8032  ax-0id 8035

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  fv0p1e1  9153  zgt0ge1  9433  nn0lt10b  9455  gtndiv  9470  nn0ind-raph  9492  1e0p1  9547  fz01en  10177  fz01or  10235  fz0tp  10246  fz0to3un2pr  10247  elfzonlteqm1  10341  fzo0to2pr  10349  fzo0to3tp  10350  fldiv4p1lem1div2  10450  mulp1mod1  10512  1tonninf  10588  expp1  10693  facp1  10877  faclbnd  10888  bcm1k  10907  bcval5  10910  bcpasc  10913  hash1  10958  binomlem  11827  isumnn0nn  11837  fprodfac  11959  ege2le3  12015  ef4p  12038  eirraplem  12121  p1modz1  12138  nn0o1gt2  12249  bitsfzo  12299  pw2dvdslemn  12520  pcfaclem  12705  4sqlem19  12765  2exp16  12793  ennnfonelemjn  12806  exmidunben  12830  gsumfzconst  13710  gsumfzsnfd  13714  dvply1  15270  lgsne0  15548  gausslemma2dlem4  15574  lgsquadlem2  15588  012of  15967  2o01f  15968  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028