Theorem 0p1e1 9240

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

Syntax hints:   = wceq 1395  (class class class)co 6010   0cc0 8015   1c1 8016   + caddc 8018

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 8108  ax-icn 8110  ax-addcl 8111  ax-mulcl 8113  ax-addcom 8115  ax-i2m1 8120  ax-0id 8123

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

This theorem is referenced by:  fv0p1e1  9241  zgt0ge1  9521  nn0lt10b  9543  gtndiv  9558  nn0ind-raph  9580  1e0p1  9635  fz01en  10266  fz01or  10324  fz0tp  10335  fz0to3un2pr  10336  elfzonlteqm1  10433  fzo0to2pr  10441  fzo0to3tp  10442  fldiv4p1lem1div2  10542  mulp1mod1  10604  1tonninf  10680  expp1  10785  facp1  10969  faclbnd  10980  bcm1k  10999  bcval5  11002  bcpasc  11005  hash1  11051  binomlem  12015  isumnn0nn  12025  fprodfac  12147  ege2le3  12203  ef4p  12226  eirraplem  12309  p1modz1  12326  nn0o1gt2  12437  bitsfzo  12487  pw2dvdslemn  12708  pcfaclem  12893  4sqlem19  12953  2exp16  12981  ennnfonelemjn  12994  exmidunben  13018  gsumfzconst  13899  gsumfzsnfd  13903  dvply1  15460  lgsne0  15738  gausslemma2dlem4  15764  lgsquadlem2  15778  wlkl1loop  16130  clwwlkccatlem  16169  umgr2cwwk2dif  16192  012of  16470  2o01f  16471  isomninnlem  16512  iswomninnlem  16531  ismkvnnlem  16534