Theorem addlidi 8222

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

Syntax hints:   = wceq 1373   e. wcel 2177  (class class class)co 5951   CCcc 7930   0cc0 7932   + caddc 7935

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-addcom 8032  ax-i2m1 8037  ax-0id 8040

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  ine0  8473  inelr  8664  muleqadd  8748  0p1e1  9157  iap0  9267  num0h  9522  nummul1c  9559  decrmac  9568  decmul1  9574  fz0tp  10251  fz0to4untppr  10253  fzo0to3tp  10355  rei  11254  imi  11255  resqrexlemover  11365  ef01bndlem  12111  5ndvds3  12289  dec5dvds2  12780  2exp11  12803  2exp16  12804  efhalfpi  15315  sinq34lt0t  15347  ex-fac  15738