Theorem 0p1e1 9428

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088   0cc0 8186   1c1 8187   + caddc 8189

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 8279  ax-icn 8281  ax-addcl 8282  ax-mulcl 8284  ax-addcom 8286  ax-i2m1 8291  ax-0id 8294

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

This theorem is used by:  fv0p1e1  9429  zgt0ge1  9715  nn0lt10b  9738  gtndiv  9753  nn0ind-raph  9775  1e0p1  9835  fz01en  10477  fz01or  10536  fz0tp  10547  fz0to3un2pr  10548  elfzonlteqm1  10646  fzo0to2pr  10654  fzo0to3tp  10655  fldiv4p1lem1div2  10762  mulp1mod1  10824  1tonninf  10900  expp1  11005  facp1  11191  faclbnd  11202  bcm1k  11221  bcval5  11224  bcpasc  11227  hash1  11275  binomlem  12276  isumnn0nn  12286  fprodfac  12408  ege2le3  12464  ef4p  12487  eirraplem  12570  p1modz1  12587  nn0o1gt2  12698  bitsfzo  12748  pwbdvdslemn  12970  pcfaclem  13158  4sqlem19  13218  2exp16  13247  37prm  13265  631prm  13271  1259lem3  13274  1259lem4  13275  ennnfonelemjn  13352  exmidunben  13376  gzsumconst  14234  gzsumsnfd  14238  dvply1  16003  efap1p  16017  log2ublem3  16235  bposlem1  16323  lgsne0  16374  gausslemma2dlem4  16400  lgsquadlem2  16414  wlkl1loop  16816  clwwlkccatlem  16858  umgr2cwwk2dif  16882  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  012of  17240  2o01f  17241  isomninnlem  17297  iswomninnlem  17318  ismkvnnlem  17321