Theorem 0p1e1 9123

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

Syntax hints:   = wceq 1364  (class class class)co 5925  0cc0 7898  1c1 7899   + caddc 7901

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-addcom 7998  ax-i2m1 8003  ax-0id 8006

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  fv0p1e1  9124  zgt0ge1  9403  nn0lt10b  9425  gtndiv  9440  nn0ind-raph  9462  1e0p1  9517  fz01en  10147  fz01or  10205  fz0tp  10216  fz0to3un2pr  10217  elfzonlteqm1  10305  fzo0to2pr  10313  fzo0to3tp  10314  fldiv4p1lem1div2  10414  mulp1mod1  10476  1tonninf  10552  expp1  10657  facp1  10841  faclbnd  10852  bcm1k  10871  bcval5  10874  bcpasc  10877  hash1  10922  binomlem  11667  isumnn0nn  11677  fprodfac  11799  ege2le3  11855  ef4p  11878  eirraplem  11961  p1modz1  11978  nn0o1gt2  12089  bitsfzo  12139  pw2dvdslemn  12360  pcfaclem  12545  4sqlem19  12605  2exp16  12633  ennnfonelemjn  12646  exmidunben  12670  gsumfzconst  13549  gsumfzsnfd  13553  dvply1  15109  lgsne0  15387  gausslemma2dlem4  15413  lgsquadlem2  15427  012of  15748  2o01f  15749  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809