Theorem 0p1e1 9096

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

Syntax hints:   = wceq 1364  (class class class)co 5918  0cc0 7872  1c1 7873   + caddc 7875

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-addcom 7972  ax-i2m1 7977  ax-0id 7980

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

This theorem is referenced by:  fv0p1e1  9097  zgt0ge1  9375  nn0lt10b  9397  gtndiv  9412  nn0ind-raph  9434  1e0p1  9489  fz01en  10119  fz01or  10177  fz0tp  10188  fz0to3un2pr  10189  elfzonlteqm1  10277  fzo0to2pr  10285  fzo0to3tp  10286  fldiv4p1lem1div2  10374  mulp1mod1  10436  1tonninf  10512  expp1  10617  facp1  10801  faclbnd  10812  bcm1k  10831  bcval5  10834  bcpasc  10837  hash1  10882  binomlem  11626  isumnn0nn  11636  fprodfac  11758  ege2le3  11814  ef4p  11837  eirraplem  11920  p1modz1  11937  nn0o1gt2  12046  pw2dvdslemn  12303  pcfaclem  12487  4sqlem19  12547  ennnfonelemjn  12559  exmidunben  12583  gsumfzconst  13411  gsumfzsnfd  13415  lgsne0  15154  gausslemma2dlem4  15180  012of  15486  2o01f  15487  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542