Theorem 0p1e1 9192

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

Syntax hints:   = wceq 1375  (class class class)co 5974   0cc0 7967   1c1 7968   + caddc 7970

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-addcom 8067  ax-i2m1 8072  ax-0id 8075

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  fv0p1e1  9193  zgt0ge1  9473  nn0lt10b  9495  gtndiv  9510  nn0ind-raph  9532  1e0p1  9587  fz01en  10217  fz01or  10275  fz0tp  10286  fz0to3un2pr  10287  elfzonlteqm1  10383  fzo0to2pr  10391  fzo0to3tp  10392  fldiv4p1lem1div2  10492  mulp1mod1  10554  1tonninf  10630  expp1  10735  facp1  10919  faclbnd  10930  bcm1k  10949  bcval5  10952  bcpasc  10955  hash1  11000  binomlem  11960  isumnn0nn  11970  fprodfac  12092  ege2le3  12148  ef4p  12171  eirraplem  12254  p1modz1  12271  nn0o1gt2  12382  bitsfzo  12432  pw2dvdslemn  12653  pcfaclem  12838  4sqlem19  12898  2exp16  12926  ennnfonelemjn  12939  exmidunben  12963  gsumfzconst  13844  gsumfzsnfd  13848  dvply1  15404  lgsne0  15682  gausslemma2dlem4  15708  lgsquadlem2  15722  012of  16268  2o01f  16269  isomninnlem  16309  iswomninnlem  16328  ismkvnnlem  16331