Theorem addlidi 8167

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

Syntax hints:   = wceq 1364   e. wcel 2167  (class class class)co 5922   CCcc 7875   0cc0 7877   + caddc 7880

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7970  ax-icn 7972  ax-addcl 7973  ax-mulcl 7975  ax-addcom 7977  ax-i2m1 7982  ax-0id 7985

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  ine0  8418  inelr  8608  muleqadd  8692  0p1e1  9101  iap0  9211  num0h  9465  nummul1c  9502  decrmac  9511  decmul1  9517  fz0tp  10194  fz0to4untppr  10196  fzo0to3tp  10292  rei  11049  imi  11050  resqrexlemover  11160  ef01bndlem  11905  dec5dvds2  12558  2exp11  12581  2exp16  12582  efhalfpi  15008  sinq34lt0t  15040  ex-fac  15341