Theorem 0p1e1 9232

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 8100	. 2 |- 1 e. CC
2	1	addlidi 8297	1 |- ( 0 + 1 ) = 1

Syntax hints:   = wceq 1395  (class class class)co 6007   0cc0 8007   1c1 8008   + caddc 8010

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8100  ax-icn 8102  ax-addcl 8103  ax-mulcl 8105  ax-addcom 8107  ax-i2m1 8112  ax-0id 8115

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  fv0p1e1  9233  zgt0ge1  9513  nn0lt10b  9535  gtndiv  9550  nn0ind-raph  9572  1e0p1  9627  fz01en  10257  fz01or  10315  fz0tp  10326  fz0to3un2pr  10327  elfzonlteqm1  10424  fzo0to2pr  10432  fzo0to3tp  10433  fldiv4p1lem1div2  10533  mulp1mod1  10595  1tonninf  10671  expp1  10776  facp1  10960  faclbnd  10971  bcm1k  10990  bcval5  10993  bcpasc  10996  hash1  11041  binomlem  12002  isumnn0nn  12012  fprodfac  12134  ege2le3  12190  ef4p  12213  eirraplem  12296  p1modz1  12313  nn0o1gt2  12424  bitsfzo  12474  pw2dvdslemn  12695  pcfaclem  12880  4sqlem19  12940  2exp16  12968  ennnfonelemjn  12981  exmidunben  13005  gsumfzconst  13886  gsumfzsnfd  13890  dvply1  15447  lgsne0  15725  gausslemma2dlem4  15751  lgsquadlem2  15765  wlkl1loop  16079  012of  16386  2o01f  16387  isomninnlem  16428  iswomninnlem  16447  ismkvnnlem  16450