Theorem 0p1e1 9033

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

Syntax hints:   = wceq 1353  (class class class)co 5875  0cc0 7811  1c1 7812   + caddc 7814

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 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-addcom 7911  ax-i2m1 7916  ax-0id 7919

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

This theorem is referenced by:  fv0p1e1  9034  zgt0ge1  9311  nn0lt10b  9333  gtndiv  9348  nn0ind-raph  9370  1e0p1  9425  fz01en  10053  fz01or  10111  fz0tp  10122  fz0to3un2pr  10123  elfzonlteqm1  10210  fzo0to2pr  10218  fzo0to3tp  10219  fldiv4p1lem1div2  10305  mulp1mod1  10365  1tonninf  10440  expp1  10527  facp1  10710  faclbnd  10721  bcm1k  10740  bcval5  10743  bcpasc  10746  hash1  10791  binomlem  11491  isumnn0nn  11501  fprodfac  11623  ege2le3  11679  ef4p  11702  eirraplem  11784  p1modz1  11801  nn0o1gt2  11910  pw2dvdslemn  12165  pcfaclem  12347  ennnfonelemjn  12403  exmidunben  12427  lgsne0  14442  012of  14748  2o01f  14749  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803