Theorem 0p1e1 9035

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

Syntax hints:   = wceq 1353  (class class class)co 5877   0cc0 7813   1c1 7814   + caddc 7816

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-addcom 7913  ax-i2m1 7918  ax-0id 7921

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  fv0p1e1  9036  zgt0ge1  9313  nn0lt10b  9335  gtndiv  9350  nn0ind-raph  9372  1e0p1  9427  fz01en  10055  fz01or  10113  fz0tp  10124  fz0to3un2pr  10125  elfzonlteqm1  10212  fzo0to2pr  10220  fzo0to3tp  10221  fldiv4p1lem1div2  10307  mulp1mod1  10367  1tonninf  10442  expp1  10529  facp1  10712  faclbnd  10723  bcm1k  10742  bcval5  10745  bcpasc  10748  hash1  10793  binomlem  11493  isumnn0nn  11503  fprodfac  11625  ege2le3  11681  ef4p  11704  eirraplem  11786  p1modz1  11803  nn0o1gt2  11912  pw2dvdslemn  12167  pcfaclem  12349  ennnfonelemjn  12405  exmidunben  12429  lgsne0  14524  012of  14830  2o01f  14831  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885