Theorem 0p1e1 8834

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 7713	. 2 ⊢ 1 ∈ ℂ
2	1	addid2i 7905	1 ⊢ (0 + 1) = 1

Syntax hints:   = wceq 1331  (class class class)co 5774  0cc0 7620  1c1 7621   + caddc 7623

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-addcom 7720  ax-i2m1 7725  ax-0id 7728

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  fv0p1e1  8835  zgt0ge1  9112  nn0lt10b  9131  gtndiv  9146  nn0ind-raph  9168  1e0p1  9223  fz01en  9833  fz01or  9891  fz0tp  9901  elfzonlteqm1  9987  fzo0to2pr  9995  fzo0to3tp  9996  fldiv4p1lem1div2  10078  mulp1mod1  10138  1tonninf  10213  expp1  10300  facp1  10476  faclbnd  10487  bcm1k  10506  bcval5  10509  bcpasc  10512  hash1  10557  binomlem  11252  isumnn0nn  11262  ege2le3  11377  ef4p  11400  eirraplem  11483  nn0o1gt2  11602  pw2dvdslemn  11843  ennnfonelemjn  11915  exmidunben  11939  isomninnlem  13225