Theorem addid2i 8113

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

Syntax hints:   = wceq 1363   e. wcel 2158  (class class class)co 5888   CCcc 7822   0cc0 7824   + caddc 7827

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1cn 7917  ax-icn 7919  ax-addcl 7920  ax-mulcl 7922  ax-addcom 7924  ax-i2m1 7929  ax-0id 7932

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  ine0  8364  inelr  8554  muleqadd  8638  0p1e1  9046  iap0  9155  num0h  9408  nummul1c  9445  decrmac  9454  decmul1  9460  fz0tp  10135  fz0to4untppr  10137  fzo0to3tp  10232  rei  10921  imi  10922  resqrexlemover  11032  ef01bndlem  11777  efhalfpi  14491  sinq34lt0t  14523  ex-fac  14751