Theorem addid2i 8131

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

Syntax hints:   = wceq 1364   ∈ wcel 2160  (class class class)co 5897  ℂcc 7840  0cc0 7842   + caddc 7845

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7935  ax-icn 7937  ax-addcl 7938  ax-mulcl 7940  ax-addcom 7942  ax-i2m1 7947  ax-0id 7950

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  ine0  8382  inelr  8572  muleqadd  8656  0p1e1  9064  iap0  9173  num0h  9426  nummul1c  9463  decrmac  9472  decmul1  9478  fz0tp  10154  fz0to4untppr  10156  fzo0to3tp  10251  rei  10943  imi  10944  resqrexlemover  11054  ef01bndlem  11799  efhalfpi  14697  sinq34lt0t  14729  ex-fac  14958