Theorem 0p1e1 9185

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

Syntax hints:   = wceq 1373  (class class class)co 5967  0cc0 7960  1c1 7961   + caddc 7963

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-mulcl 8058  ax-addcom 8060  ax-i2m1 8065  ax-0id 8068

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  fv0p1e1  9186  zgt0ge1  9466  nn0lt10b  9488  gtndiv  9503  nn0ind-raph  9525  1e0p1  9580  fz01en  10210  fz01or  10268  fz0tp  10279  fz0to3un2pr  10280  elfzonlteqm1  10376  fzo0to2pr  10384  fzo0to3tp  10385  fldiv4p1lem1div2  10485  mulp1mod1  10547  1tonninf  10623  expp1  10728  facp1  10912  faclbnd  10923  bcm1k  10942  bcval5  10945  bcpasc  10948  hash1  10993  binomlem  11909  isumnn0nn  11919  fprodfac  12041  ege2le3  12097  ef4p  12120  eirraplem  12203  p1modz1  12220  nn0o1gt2  12331  bitsfzo  12381  pw2dvdslemn  12602  pcfaclem  12787  4sqlem19  12847  2exp16  12875  ennnfonelemjn  12888  exmidunben  12912  gsumfzconst  13792  gsumfzsnfd  13796  dvply1  15352  lgsne0  15630  gausslemma2dlem4  15656  lgsquadlem2  15670  012of  16130  2o01f  16131  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193