Theorem addlidi 8188

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

Syntax hints:   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896  0cc0 7898   + caddc 7901

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-addcom 7998  ax-i2m1 8003  ax-0id 8006

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  ine0  8439  inelr  8630  muleqadd  8714  0p1e1  9123  iap0  9233  num0h  9487  nummul1c  9524  decrmac  9533  decmul1  9539  fz0tp  10216  fz0to4untppr  10218  fzo0to3tp  10314  rei  11083  imi  11084  resqrexlemover  11194  ef01bndlem  11940  5ndvds3  12118  dec5dvds2  12609  2exp11  12632  2exp16  12633  efhalfpi  15143  sinq34lt0t  15175  ex-fac  15482