Theorem addid2i 7929

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

Syntax hints:   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   0cc0 7644   + caddc 7647

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-addcom 7744  ax-i2m1 7749  ax-0id 7752

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  ine0  8180  inelr  8370  muleqadd  8453  0p1e1  8858  iap0  8967  num0h  9217  nummul1c  9254  decrmac  9263  decmul1  9269  fz0tp  9932  fzo0to3tp  10027  rei  10703  imi  10704  resqrexlemover  10814  ef01bndlem  11499  efhalfpi  12928  sinq34lt0t  12960  ex-fac  13111