Theorem 0p1e1 8992

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 7867	. 2 |- 1 e. CC
2	1	addid2i 8062	1 |- ( 0 + 1 ) = 1

Syntax hints:   = wceq 1348  (class class class)co 5853   0cc0 7774   1c1 7775   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-addcom 7874  ax-i2m1 7879  ax-0id 7882

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  fv0p1e1  8993  zgt0ge1  9270  nn0lt10b  9292  gtndiv  9307  nn0ind-raph  9329  1e0p1  9384  fz01en  10009  fz01or  10067  fz0tp  10078  fz0to3un2pr  10079  elfzonlteqm1  10166  fzo0to2pr  10174  fzo0to3tp  10175  fldiv4p1lem1div2  10261  mulp1mod1  10321  1tonninf  10396  expp1  10483  facp1  10664  faclbnd  10675  bcm1k  10694  bcval5  10697  bcpasc  10700  hash1  10746  binomlem  11446  isumnn0nn  11456  fprodfac  11578  ege2le3  11634  ef4p  11657  eirraplem  11739  p1modz1  11756  nn0o1gt2  11864  pw2dvdslemn  12119  pcfaclem  12301  ennnfonelemjn  12357  exmidunben  12381  lgsne0  13733  012of  14028  2o01f  14029  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084