Theorem 00id 8255

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

Syntax hints:   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   + caddc 7970

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-i2m1 8072  ax-0id 8075

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  negdii  8398  addgt0  8563  addgegt0  8564  addgtge0  8565  addge0  8566  add20  8589  recexaplem2  8767  crap0  9073  iap0  9302  decaddm10  9604  10p10e20  9640  ser0  10722  bcpasc  10955  abs00ap  11539  fsumadd  11883  fsumrelem  11948  arisum  11975  bezoutr1  12520  nnnn0modprm0  12744  pcaddlem  12828  4sqlem19  12898  cnfld0  14500  1kp2ke3k  15998