Theorem addid2i 8049

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

Syntax hints:   = wceq 1348   e. wcel 2141  (class class class)co 5850   CCcc 7759   0cc0 7761   + caddc 7764

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7854  ax-icn 7856  ax-addcl 7857  ax-mulcl 7859  ax-addcom 7861  ax-i2m1 7866  ax-0id 7869

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  ine0  8300  inelr  8490  muleqadd  8573  0p1e1  8979  iap0  9088  num0h  9341  nummul1c  9378  decrmac  9387  decmul1  9393  fz0tp  10065  fz0to4untppr  10067  fzo0to3tp  10162  rei  10850  imi  10851  resqrexlemover  10961  ef01bndlem  11706  efhalfpi  13435  sinq34lt0t  13467  ex-fac  13684