Theorem 0p1e1 8971

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

Syntax hints:   = wceq 1343  (class class class)co 5842  0cc0 7753  1c1 7754   + caddc 7756

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1cn 7846  ax-icn 7848  ax-addcl 7849  ax-mulcl 7851  ax-addcom 7853  ax-i2m1 7858  ax-0id 7861

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  fv0p1e1  8972  zgt0ge1  9249  nn0lt10b  9271  gtndiv  9286  nn0ind-raph  9308  1e0p1  9363  fz01en  9988  fz01or  10046  fz0tp  10057  fz0to3un2pr  10058  elfzonlteqm1  10145  fzo0to2pr  10153  fzo0to3tp  10154  fldiv4p1lem1div2  10240  mulp1mod1  10300  1tonninf  10375  expp1  10462  facp1  10643  faclbnd  10654  bcm1k  10673  bcval5  10676  bcpasc  10679  hash1  10724  binomlem  11424  isumnn0nn  11434  fprodfac  11556  ege2le3  11612  ef4p  11635  eirraplem  11717  p1modz1  11734  nn0o1gt2  11842  pw2dvdslemn  12097  pcfaclem  12279  ennnfonelemjn  12335  exmidunben  12359  lgsne0  13579  012of  13875  2o01f  13876  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931