Theorem 0p1e1 8744

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

Syntax hints:   = wceq 1314  (class class class)co 5728  0cc0 7547  1c1 7548   + caddc 7550

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1cn 7638  ax-icn 7640  ax-addcl 7641  ax-mulcl 7643  ax-addcom 7645  ax-i2m1 7650  ax-0id 7653

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  fv0p1e1  8745  zgt0ge1  9016  nn0lt10b  9035  gtndiv  9050  nn0ind-raph  9072  1e0p1  9127  fz01en  9726  fz01or  9784  fz0tp  9794  elfzonlteqm1  9880  fzo0to2pr  9888  fzo0to3tp  9889  fldiv4p1lem1div2  9971  mulp1mod1  10031  1tonninf  10106  expp1  10193  facp1  10369  faclbnd  10380  bcm1k  10399  bcval5  10402  bcpasc  10405  hash1  10450  binomlem  11144  isumnn0nn  11154  ege2le3  11228  ef4p  11251  eirraplem  11331  nn0o1gt2  11450  pw2dvdslemn  11688  ennnfonelemjn  11760  exmidunben  11784  isomninnlem  12917