Theorem 0p1e1 9418

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 8272	. 2 ⊢ 1 ∈ ℂ
2	1	addlidi 8469	1 ⊢ (0 + 1) = 1

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

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 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-addcom 8279  ax-i2m1 8284  ax-0id 8287

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

This theorem is used by:  fv0p1e1  9419  zgt0ge1  9703  nn0lt10b  9726  gtndiv  9741  nn0ind-raph  9763  1e0p1  9818  fz01en  10459  fz01or  10518  fz0tp  10529  fz0to3un2pr  10530  elfzonlteqm1  10628  fzo0to2pr  10636  fzo0to3tp  10637  fldiv4p1lem1div2  10740  mulp1mod1  10802  1tonninf  10878  expp1  10983  facp1  11168  faclbnd  11179  bcm1k  11198  bcval5  11201  bcpasc  11204  hash1  11252  binomlem  12250  isumnn0nn  12260  fprodfac  12382  ege2le3  12438  ef4p  12461  eirraplem  12544  p1modz1  12561  nn0o1gt2  12672  bitsfzo  12722  pw2dvdslemn  12943  pcfaclem  13128  4sqlem19  13188  2exp16  13216  ennnfonelemjn  13293  exmidunben  13317  gzsumconst  14143  gzsumsnfd  14147  dvply1  15866  log2ublem3  16085  lgsne0  16157  gausslemma2dlem4  16183  lgsquadlem2  16197  wlkl1loop  16599  clwwlkccatlem  16641  umgr2cwwk2dif  16665  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  012of  17023  2o01f  17024  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102