Theorem addlidi 8186

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

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

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 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-addcom 7996  ax-i2m1 8001  ax-0id 8004

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

This theorem is referenced by:  ine0  8437  inelr  8628  muleqadd  8712  0p1e1  9121  iap0  9231  num0h  9485  nummul1c  9522  decrmac  9531  decmul1  9537  fz0tp  10214  fz0to4untppr  10216  fzo0to3tp  10312  rei  11081  imi  11082  resqrexlemover  11192  ef01bndlem  11938  5ndvds3  12116  dec5dvds2  12607  2exp11  12630  2exp16  12631  efhalfpi  15119  sinq34lt0t  15151  ex-fac  15458