Theorem addlidi 8421

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 8417	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (0 + 𝐴) = 𝐴

Syntax hints:   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130  0cc0 8132   + caddc 8135

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 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-addcom 8232  ax-i2m1 8237  ax-0id 8240

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

This theorem is referenced by:  ine0  8672  inelr  8863  muleqadd  8947  0p1e1  9356  iap0  9466  num0h  9726  nummul1c  9763  decrmac  9772  decmul1  9778  fz0tp  10463  fz0to4untppr  10465  fzo0to3tp  10571  cats1fvn  11464  rei  11592  imi  11593  resqrexlemover  11703  ef01bndlem  12450  5ndvds3  12628  dec5dvds2  13119  2exp11  13142  2exp16  13143  efhalfpi  15713  sinq34lt0t  15745  ex-fac  16545