Theorem addlidi 8434

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 8430	. 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 6059   CCcc 8142   0cc0 8144   + caddc 8147

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 8237  ax-icn 8239  ax-addcl 8240  ax-mulcl 8242  ax-addcom 8244  ax-i2m1 8249  ax-0id 8252

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

This theorem is referenced by:  ine0  8686  inelr  8877  muleqadd  8963  0p1e1  9372  iap0  9482  num0h  9742  nummul1c  9779  decrmac  9788  decmul1  9794  fz0tp  10482  fz0to4untppr  10484  fzo0to3tp  10590  cats1fvn  11485  rei  11614  imi  11615  resqrexlemover  11725  ef01bndlem  12472  5ndvds3  12650  dec5dvds2  13141  2exp11  13164  2exp16  13165  efhalfpi  15795  sinq34lt0t  15827  ex-fac  16627