Theorem addlidi 8415

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

Syntax hints:   = wceq 1398   e. wcel 2203  (class class class)co 6049   CCcc 8124   0cc0 8126   + caddc 8129

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 2214  ax-1cn 8219  ax-icn 8221  ax-addcl 8222  ax-mulcl 8224  ax-addcom 8226  ax-i2m1 8231  ax-0id 8234

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  ine0  8666  inelr  8857  muleqadd  8941  0p1e1  9350  iap0  9460  num0h  9719  nummul1c  9756  decrmac  9765  decmul1  9771  fz0tp  10455  fz0to4untppr  10457  fzo0to3tp  10563  cats1fvn  11452  rei  11580  imi  11581  resqrexlemover  11691  ef01bndlem  12438  5ndvds3  12616  dec5dvds2  13107  2exp11  13130  2exp16  13131  efhalfpi  15656  sinq34lt0t  15688  ex-fac  16488