Theorem 0p1e1 8962

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 7837	. 2 ⊢ 1 ∈ ℂ
2	1	addid2i 8032	1 ⊢ (0 + 1) = 1

Syntax hints:   = wceq 1342  (class class class)co 5836  0cc0 7744  1c1 7745   + caddc 7747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146  ax-1cn 7837  ax-icn 7839  ax-addcl 7840  ax-mulcl 7842  ax-addcom 7844  ax-i2m1 7849  ax-0id 7852

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160

This theorem is referenced by:  fv0p1e1  8963  zgt0ge1  9240  nn0lt10b  9262  gtndiv  9277  nn0ind-raph  9299  1e0p1  9354  fz01en  9978  fz01or  10036  fz0tp  10047  fz0to3un2pr  10048  elfzonlteqm1  10135  fzo0to2pr  10143  fzo0to3tp  10144  fldiv4p1lem1div2  10230  mulp1mod1  10290  1tonninf  10365  expp1  10452  facp1  10632  faclbnd  10643  bcm1k  10662  bcval5  10665  bcpasc  10668  hash1  10713  binomlem  11410  isumnn0nn  11420  fprodfac  11542  ege2le3  11598  ef4p  11621  eirraplem  11703  p1modz1  11720  nn0o1gt2  11827  pw2dvdslemn  12074  pcfaclem  12256  ennnfonelemjn  12272  exmidunben  12296  012of  13709  2o01f  13710  isomninnlem  13743  iswomninnlem  13762  ismkvnnlem  13765