Theorem 0p1e1 9421

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085   0cc0 8180   1c1 8181   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-addcom 8280  ax-i2m1 8285  ax-0id 8288

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  fv0p1e1  9422  zgt0ge1  9708  nn0lt10b  9731  gtndiv  9746  nn0ind-raph  9768  1e0p1  9828  fz01en  10470  fz01or  10529  fz0tp  10540  fz0to3un2pr  10541  elfzonlteqm1  10639  fzo0to2pr  10647  fzo0to3tp  10648  fldiv4p1lem1div2  10754  mulp1mod1  10816  1tonninf  10892  expp1  10997  facp1  11183  faclbnd  11194  bcm1k  11213  bcval5  11216  bcpasc  11219  hash1  11267  binomlem  12268  isumnn0nn  12278  fprodfac  12400  ege2le3  12456  ef4p  12479  eirraplem  12562  p1modz1  12579  nn0o1gt2  12690  bitsfzo  12740  pwbdvdslemn  12962  pcfaclem  13150  4sqlem19  13210  2exp16  13239  37prm  13257  631prm  13263  1259lem3  13266  1259lem4  13267  ennnfonelemjn  13344  exmidunben  13368  gzsumconst  14194  gzsumsnfd  14198  dvply1  15918  efap1p  15932  log2ublem3  16145  bposlem1  16233  lgsne0  16279  gausslemma2dlem4  16305  lgsquadlem2  16319  wlkl1loop  16721  clwwlkccatlem  16763  umgr2cwwk2dif  16787  konigsberglem1  16851  konigsberglem2  16852  konigsberglem3  16853  012of  17145  2o01f  17146  isomninnlem  17201  iswomninnlem  17221  ismkvnnlem  17224