Theorem 0p1e1 9247

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

Syntax hints:   = wceq 1395  (class class class)co 6013  0cc0 8022  1c1 8023   + caddc 8025

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 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-addcom 8122  ax-i2m1 8127  ax-0id 8130

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

This theorem is referenced by:  fv0p1e1  9248  zgt0ge1  9528  nn0lt10b  9550  gtndiv  9565  nn0ind-raph  9587  1e0p1  9642  fz01en  10278  fz01or  10336  fz0tp  10347  fz0to3un2pr  10348  elfzonlteqm1  10445  fzo0to2pr  10453  fzo0to3tp  10454  fldiv4p1lem1div2  10555  mulp1mod1  10617  1tonninf  10693  expp1  10798  facp1  10982  faclbnd  10993  bcm1k  11012  bcval5  11015  bcpasc  11018  hash1  11065  binomlem  12034  isumnn0nn  12044  fprodfac  12166  ege2le3  12222  ef4p  12245  eirraplem  12328  p1modz1  12345  nn0o1gt2  12456  bitsfzo  12506  pw2dvdslemn  12727  pcfaclem  12912  4sqlem19  12972  2exp16  13000  ennnfonelemjn  13013  exmidunben  13037  gsumfzconst  13918  gsumfzsnfd  13922  dvply1  15479  lgsne0  15757  gausslemma2dlem4  15783  lgsquadlem2  15797  wlkl1loop  16155  clwwlkccatlem  16195  umgr2cwwk2dif  16219  012of  16528  2o01f  16529  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592