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 ∈ ℂ
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  10755  mulp1mod1  10817  1tonninf  10893  expp1  10998  facp1  11184  faclbnd  11195  bcm1k  11214  bcval5  11217  bcpasc  11220  hash1  11268  binomlem  12269  isumnn0nn  12279  fprodfac  12401  ege2le3  12457  ef4p  12480  eirraplem  12563  p1modz1  12580  nn0o1gt2  12691  bitsfzo  12741  pwbdvdslemn  12963  pcfaclem  13151  4sqlem19  13211  2exp16  13240  37prm  13258  631prm  13264  1259lem3  13267  1259lem4  13268  ennnfonelemjn  13345  exmidunben  13369  gzsumconst  14227  gzsumsnfd  14231  dvply1  15957  efap1p  15971  log2ublem3  16184  bposlem1  16272  lgsne0  16323  gausslemma2dlem4  16349  lgsquadlem2  16363  wlkl1loop  16765  clwwlkccatlem  16807  umgr2cwwk2dif  16831  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  012of  17189  2o01f  17190  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269