Theorem 00id 8325

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 8176	. 2 ⊢ 0 ∈ ℂ
2		addrid 8322	. 2 ⊢ (0 ∈ ℂ → (0 + 0) = 0)
3	1, 2	ax-mp 5	1 ⊢ (0 + 0) = 0

Syntax hints:   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035  0cc0 8037   + caddc 8040

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2212  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-i2m1 8142  ax-0id 8145

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226

This theorem is referenced by:  negdii  8468  addgt0  8633  addgegt0  8634  addgtge0  8635  addge0  8636  add20  8659  recexaplem2  8837  crap0  9143  iap0  9372  decaddm10  9674  10p10e20  9710  ser0  10801  bcpasc  11034  abs00ap  11645  fsumadd  11990  fsumrelem  12055  arisum  12082  bezoutr1  12627  nnnn0modprm0  12851  pcaddlem  12935  4sqlem19  13005  cnfld0  14609  vtxdgfi0e  16175  1kp2ke3k  16377