Theorem addlidi 8432

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
addlidi	|- ( 0 + A ) = A

Proof of Theorem addlidi

Step	Hyp	Ref	Expression
1		mul.1	. 2 |- A e. CC
2		addlid 8428	. 2 |- ( A e. CC -> ( 0 + A ) = A )
3	1, 2	ax-mp 5	1 |- ( 0 + A ) = A

Syntax hints:   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  ine0  8684  inelr  8875  muleqadd  8959  0p1e1  9368  iap0  9478  num0h  9738  nummul1c  9775  decrmac  9784  decmul1  9790  fz0tp  10478  fz0to4untppr  10480  fzo0to3tp  10586  cats1fvn  11481  rei  11609  imi  11610  resqrexlemover  11720  ef01bndlem  12467  5ndvds3  12645  dec5dvds2  13136  2exp11  13159  2exp16  13160  efhalfpi  15776  sinq34lt0t  15808  ex-fac  16608