Theorem 0p1e1 9427

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 8278	. 2 ⊢ 1 ∈ ℂ
2	1	addlidi 8476	1 ⊢ (0 + 1) = 1

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088  0cc0 8185  1c1 8186   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-addcom 8285  ax-i2m1 8290  ax-0id 8293

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  fv0p1e1  9428  zgt0ge1  9714  nn0lt10b  9737  gtndiv  9752  nn0ind-raph  9774  1e0p1  9834  fz01en  10476  fz01or  10535  fz0tp  10546  fz0to3un2pr  10547  elfzonlteqm1  10645  fzo0to2pr  10653  fzo0to3tp  10654  fldiv4p1lem1div2  10761  mulp1mod1  10823  1tonninf  10899  expp1  11004  facp1  11190  faclbnd  11201  bcm1k  11220  bcval5  11223  bcpasc  11226  hash1  11274  binomlem  12275  isumnn0nn  12285  fprodfac  12407  ege2le3  12463  ef4p  12486  eirraplem  12569  p1modz1  12586  nn0o1gt2  12697  bitsfzo  12747  pwbdvdslemn  12969  pcfaclem  13157  4sqlem19  13217  2exp16  13246  37prm  13264  631prm  13270  1259lem3  13273  1259lem4  13274  ennnfonelemjn  13351  exmidunben  13375  gzsumconst  14233  gzsumsnfd  14237  dvply1  15991  efap1p  16005  log2ublem3  16223  bposlem1  16311  lgsne0  16362  gausslemma2dlem4  16388  lgsquadlem2  16402  wlkl1loop  16804  clwwlkccatlem  16846  umgr2cwwk2dif  16870  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  012of  17228  2o01f  17229  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309