Theorem 00id 7316

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 7173	. 2 ⊢ 0 ∈ ℂ
2		addid1 7313	. 2 ⊢ (0 ∈ ℂ → (0 + 0) = 0)
3	1, 2	ax-mp 7	1 ⊢ (0 + 0) = 0

Syntax hints:   = wceq 1285   ∈ wcel 1434  (class class class)co 5543  ℂcc 7041  0cc0 7043   + caddc 7046

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1cn 7131  ax-icn 7133  ax-addcl 7134  ax-mulcl 7136  ax-i2m1 7143  ax-0id 7146

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078

This theorem is referenced by:  negdii  7459  addgt0  7619  addgegt0  7620  addgtge0  7621  addge0  7622  add20  7645  recexaplem2  7809  crap0  8102  iap0  8321  decaddm10  8616  10p10e20  8652  iser0  9568  bcpasc  9790  abs00ap  10086  bezoutr1  10566  1kp2ke3k  10713