Theorem 0p1e1 9220

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

Syntax hints:   = wceq 1395  (class class class)co 6000   0cc0 7995   1c1 7996   + caddc 7998

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 8088  ax-icn 8090  ax-addcl 8091  ax-mulcl 8093  ax-addcom 8095  ax-i2m1 8100  ax-0id 8103

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

This theorem is referenced by:  fv0p1e1  9221  zgt0ge1  9501  nn0lt10b  9523  gtndiv  9538  nn0ind-raph  9560  1e0p1  9615  fz01en  10245  fz01or  10303  fz0tp  10314  fz0to3un2pr  10315  elfzonlteqm1  10411  fzo0to2pr  10419  fzo0to3tp  10420  fldiv4p1lem1div2  10520  mulp1mod1  10582  1tonninf  10658  expp1  10763  facp1  10947  faclbnd  10958  bcm1k  10977  bcval5  10980  bcpasc  10983  hash1  11028  binomlem  11989  isumnn0nn  11999  fprodfac  12121  ege2le3  12177  ef4p  12200  eirraplem  12283  p1modz1  12300  nn0o1gt2  12411  bitsfzo  12461  pw2dvdslemn  12682  pcfaclem  12867  4sqlem19  12927  2exp16  12955  ennnfonelemjn  12968  exmidunben  12992  gsumfzconst  13873  gsumfzsnfd  13877  dvply1  15433  lgsne0  15711  gausslemma2dlem4  15737  lgsquadlem2  15751  012of  16316  2o01f  16317  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379