Theorem 0p1e1 9356

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

Syntax hints:   = wceq 1398  (class class class)co 6052   0cc0 8132   1c1 8133   + caddc 8135

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-addcom 8232  ax-i2m1 8237  ax-0id 8240

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  fv0p1e1  9357  zgt0ge1  9641  nn0lt10b  9664  gtndiv  9679  nn0ind-raph  9701  1e0p1  9756  fz01en  10393  fz01or  10452  fz0tp  10463  fz0to3un2pr  10464  elfzonlteqm1  10562  fzo0to2pr  10570  fzo0to3tp  10571  fldiv4p1lem1div2  10672  mulp1mod1  10734  1tonninf  10810  expp1  10915  facp1  11100  faclbnd  11111  bcm1k  11130  bcval5  11133  bcpasc  11136  hash1  11184  binomlem  12177  isumnn0nn  12187  fprodfac  12309  ege2le3  12365  ef4p  12388  eirraplem  12471  p1modz1  12488  nn0o1gt2  12599  bitsfzo  12649  pw2dvdslemn  12870  pcfaclem  13055  4sqlem19  13115  2exp16  13143  ennnfonelemjn  13174  exmidunben  13198  gsumfzconst  14079  gsumfzsnfd  14083  dvply1  15679  lgsne0  15960  gausslemma2dlem4  15986  lgsquadlem2  16000  wlkl1loop  16402  clwwlkccatlem  16444  umgr2cwwk2dif  16468  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  012of  16816  2o01f  16817  isomninnlem  16863  iswomninnlem  16883  ismkvnnlem  16886