Theorem 0p1e1 9098

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 7967	. 2 |- 1 e. CC
2	1	addid2i 8164	1 |- ( 0 + 1 ) = 1

Syntax hints:   = wceq 1364  (class class class)co 5919   0cc0 7874   1c1 7875   + caddc 7877

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 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-addcom 7974  ax-i2m1 7979  ax-0id 7982

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

This theorem is referenced by:  fv0p1e1  9099  zgt0ge1  9378  nn0lt10b  9400  gtndiv  9415  nn0ind-raph  9437  1e0p1  9492  fz01en  10122  fz01or  10180  fz0tp  10191  fz0to3un2pr  10192  elfzonlteqm1  10280  fzo0to2pr  10288  fzo0to3tp  10289  fldiv4p1lem1div2  10377  mulp1mod1  10439  1tonninf  10515  expp1  10620  facp1  10804  faclbnd  10815  bcm1k  10834  bcval5  10837  bcpasc  10840  hash1  10885  binomlem  11629  isumnn0nn  11639  fprodfac  11761  ege2le3  11817  ef4p  11840  eirraplem  11923  p1modz1  11940  nn0o1gt2  12049  pw2dvdslemn  12306  pcfaclem  12490  4sqlem19  12550  ennnfonelemjn  12562  exmidunben  12586  gsumfzconst  13414  gsumfzsnfd  13418  dvply1  14943  lgsne0  15195  gausslemma2dlem4  15221  lgsquadlem2  15235  012of  15556  2o01f  15557  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612