Theorem 00id 8431

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
00id	⊢ (0 + 0) = 0

Proof of Theorem 00id

Step	Hyp	Ref	Expression
1		0cn 8282	. 2 ⊢ 0 ∈ ℂ
2		addrid 8428	. 2 ⊢ (0 ∈ ℂ → (0 + 0) = 0)
3	1, 2	ax-mp 5	1 ⊢ (0 + 0) = 0

Syntax hints:   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141  0cc0 8143   + caddc 8146

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  negdii  8574  addgt0  8740  addgegt0  8741  addgtge0  8742  addge0  8743  add20  8766  recexaplem2  8944  crap0  9252  iap0  9481  decaddm10  9788  10p10e20  9824  ser0  10922  bcpasc  11156  abs00ap  11775  fsumadd  12120  fsumrelem  12185  arisum  12212  bezoutr1  12757  nnnn0modprm0  12981  pcaddlem  13065  4sqlem19  13135  cnfld0  14848  vtxdgfi0e  16419  1kp2ke3k  16621