Theorem addid2i 7822

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

Syntax hints:   = wceq 1312   ∈ wcel 1461  (class class class)co 5726  ℂcc 7539  0cc0 7541   + caddc 7544

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095  ax-1cn 7632  ax-icn 7634  ax-addcl 7635  ax-mulcl 7637  ax-addcom 7639  ax-i2m1 7644  ax-0id 7647

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109

This theorem is referenced by:  ine0  8069  inelr  8258  muleqadd  8336  0p1e1  8738  iap0  8841  num0h  9091  nummul1c  9128  decrmac  9137  decmul1  9143  fz0tp  9788  fzo0to3tp  9883  rei  10558  imi  10559  resqrexlemover  10668  ef01bndlem  11308  ex-fac  12624