Theorem addid2i 8062

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

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addid2i	⊢ (0 + 𝐴) = 𝐴

Proof of Theorem addid2i

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

Syntax hints:   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772  0cc0 7774   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-addcom 7874  ax-i2m1 7879  ax-0id 7882

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  ine0  8313  inelr  8503  muleqadd  8586  0p1e1  8992  iap0  9101  num0h  9354  nummul1c  9391  decrmac  9400  decmul1  9406  fz0tp  10078  fz0to4untppr  10080  fzo0to3tp  10175  rei  10863  imi  10864  resqrexlemover  10974  ef01bndlem  11719  efhalfpi  13514  sinq34lt0t  13546  ex-fac  13763