Theorem 0p1e1 9004

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

Syntax hints:   = wceq 1353  (class class class)co 5865  0cc0 7786  1c1 7787   + caddc 7789

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157  ax-1cn 7879  ax-icn 7881  ax-addcl 7882  ax-mulcl 7884  ax-addcom 7886  ax-i2m1 7891  ax-0id 7894

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  fv0p1e1  9005  zgt0ge1  9282  nn0lt10b  9304  gtndiv  9319  nn0ind-raph  9341  1e0p1  9396  fz01en  10021  fz01or  10079  fz0tp  10090  fz0to3un2pr  10091  elfzonlteqm1  10178  fzo0to2pr  10186  fzo0to3tp  10187  fldiv4p1lem1div2  10273  mulp1mod1  10333  1tonninf  10408  expp1  10495  facp1  10676  faclbnd  10687  bcm1k  10706  bcval5  10709  bcpasc  10712  hash1  10757  binomlem  11457  isumnn0nn  11467  fprodfac  11589  ege2le3  11645  ef4p  11668  eirraplem  11750  p1modz1  11767  nn0o1gt2  11875  pw2dvdslemn  12130  pcfaclem  12312  ennnfonelemjn  12368  exmidunben  12392  lgsne0  13990  012of  14285  2o01f  14286  isomninnlem  14319  iswomninnlem  14338  ismkvnnlem  14341