Theorem addid2i 7623

Description: 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)

Hypothesis

Ref	Expression
mul.1	|- A e. CC

Assertion

Ref	Expression
addid2i	|- ( 0 + A ) = A

Proof of Theorem addid2i

Step	Hyp	Ref	Expression
1		mul.1	. 2 |- A e. CC
2		addid2 7619	. 2 |- ( A e. CC -> ( 0 + A ) = A )
3	1, 2	ax-mp 7	1 |- ( 0 + A ) = A

Syntax hints:   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7346   0cc0 7348   + caddc 7351

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7436  ax-icn 7438  ax-addcl 7439  ax-mulcl 7441  ax-addcom 7443  ax-i2m1 7448  ax-0id 7451

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  ine0  7870  inelr  8059  muleqadd  8135  0p1e1  8534  iap0  8637  num0h  8886  nummul1c  8923  decrmac  8932  decmul1  8938  fz0tp  9531  fzo0to3tp  9626  rei  10329  imi  10330  resqrexlemover  10439  ef01bndlem  11043  ex-fac  11610