Theorem 0p1e1 9032

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

Syntax hints:   = wceq 1353  (class class class)co 5874  0cc0 7810  1c1 7811   + caddc 7813

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 7903  ax-icn 7905  ax-addcl 7906  ax-mulcl 7908  ax-addcom 7910  ax-i2m1 7915  ax-0id 7918

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

This theorem is referenced by:  fv0p1e1  9033  zgt0ge1  9310  nn0lt10b  9332  gtndiv  9347  nn0ind-raph  9369  1e0p1  9424  fz01en  10052  fz01or  10110  fz0tp  10121  fz0to3un2pr  10122  elfzonlteqm1  10209  fzo0to2pr  10217  fzo0to3tp  10218  fldiv4p1lem1div2  10304  mulp1mod1  10364  1tonninf  10439  expp1  10526  facp1  10709  faclbnd  10720  bcm1k  10739  bcval5  10742  bcpasc  10745  hash1  10790  binomlem  11490  isumnn0nn  11500  fprodfac  11622  ege2le3  11678  ef4p  11701  eirraplem  11783  p1modz1  11800  nn0o1gt2  11909  pw2dvdslemn  12164  pcfaclem  12346  ennnfonelemjn  12402  exmidunben  12426  lgsne0  14409  012of  14715  2o01f  14716  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770