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  9713  nn0lt10b  9736  gtndiv  9752  nn0ind-raph  9774  1e0p1  9834  fz01en  10476  fz01or  10535  fz0tp  10546  fz0to3un2pr  10547  elfzonlteqm1  10645  fzo0to2pr  10653  fzo0to3tp  10654  fldiv4p1lem1div2  10761  mulp1mod1  10823  1tonninf  10899  expp1  11004  facp1  11190  faclbnd  11201  bcm1k  11220  bcval5  11223  bcpasc  11226  hash1  11274  binomlem  12275  isumnn0nn  12285  fprodfac  12407  ege2le3  12463  ef4p  12486  eirraplem  12569  p1modz1  12586  nn0o1gt2  12697  bitsfzo  12747  pwbdvdslemn  12969  pcfaclem  13157  4sqlem19  13217  2exp16  13246  37prm  13264  631prm  13270  1259lem3  13273  1259lem4  13274  ennnfonelemjn  13351  exmidunben  13375  gzsumconst  14233  gzsumsnfd  14237  dvply1  16024  efap1p  16038  log2ublem3  16256  bposlem1  16344  lgsne0  16395  gausslemma2dlem4  16421  lgsquadlem2  16435  wlkl1loop  16837  clwwlkccatlem  16879  umgr2cwwk2dif  16903  konigsberglem1  16967  konigsberglem2  16968  konigsberglem3  16969  012of  17261  2o01f  17262  isomninnlem  17318  iswomninnlem  17339  ismkvnnlem  17342