Theorem addid2i 7905

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 7901	. 2 |- ( A e. CC -> ( 0 + A ) = A )
3	1, 2	ax-mp 5	1 |- ( 0 + A ) = A

Syntax hints:   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   0cc0 7620   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-addcom 7720  ax-i2m1 7725  ax-0id 7728

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  ine0  8156  inelr  8346  muleqadd  8429  0p1e1  8834  iap0  8943  num0h  9193  nummul1c  9230  decrmac  9239  decmul1  9245  fz0tp  9901  fzo0to3tp  9996  rei  10671  imi  10672  resqrexlemover  10782  ef01bndlem  11463  efhalfpi  12880  sinq34lt0t  12912  ex-fac  12940