Theorem addid2i 8114

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 8110	. 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 7823   0cc0 7825   + caddc 7828

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 7918  ax-icn 7920  ax-addcl 7921  ax-mulcl 7923  ax-addcom 7925  ax-i2m1 7930  ax-0id 7933

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

This theorem is referenced by:  ine0  8365  inelr  8555  muleqadd  8639  0p1e1  9047  iap0  9156  num0h  9409  nummul1c  9446  decrmac  9455  decmul1  9461  fz0tp  10136  fz0to4untppr  10138  fzo0to3tp  10233  rei  10922  imi  10923  resqrexlemover  11033  ef01bndlem  11778  efhalfpi  14573  sinq34lt0t  14605  ex-fac  14833