Theorem 0p1e1 8153

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

Syntax hints:   = wceq 1284  (class class class)co 5532   0cc0 6981   1c1 6982   + caddc 6984

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-mulcl 7074  ax-addcom 7076  ax-i2m1 7081  ax-0id 7084

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  zgt0ge1  8409  nn0lt10b  8428  gtndiv  8442  nn0ind-raph  8464  1e0p1  8518  fz01en  9072  fz0tp  9135  elfzonlteqm1  9219  fzo0to2pr  9227  fzo0to3tp  9228  fldiv4p1lem1div2  9307  mulp1mod1  9367  expp1  9483  facp1  9657  faclbnd  9668  bcm1k  9687  ibcval5  9690  bcpasc  9693  fz01or  10278  nn0o1gt2  10305  pw2dvdslemn  10543