Theorem addlidi 8305

Description: 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addlidi	⊢ (0 + 𝐴) = 𝐴

Proof of Theorem addlidi

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		addlid 8301	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (0 + 𝐴) = 𝐴

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013  0cc0 8015   + caddc 8018

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8108  ax-icn 8110  ax-addcl 8111  ax-mulcl 8113  ax-addcom 8115  ax-i2m1 8120  ax-0id 8123

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

This theorem is referenced by:  ine0  8556  inelr  8747  muleqadd  8831  0p1e1  9240  iap0  9350  num0h  9605  nummul1c  9642  decrmac  9651  decmul1  9657  fz0tp  10335  fz0to4untppr  10337  fzo0to3tp  10442  cats1fvn  11317  rei  11431  imi  11432  resqrexlemover  11542  ef01bndlem  12288  5ndvds3  12466  dec5dvds2  12957  2exp11  12980  2exp16  12981  efhalfpi  15494  sinq34lt0t  15526  ex-fac  16201