Theorem addid1d 8106

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid1d	⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addid1 8095	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809  0cc0 7811   + caddc 7814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7919

This theorem is referenced by:  subsub2  8185  negsub  8205  ltaddneg  8381  ltaddpos  8409  addge01  8429  add20  8431  apreap  8544  nnge1  8942  nnnn0addcl  9206  un0addcl  9209  peano2z  9289  zaddcl  9293  uzaddcl  9586  xaddid1  9862  fzosubel3  10196  expadd  10562  faclbnd6  10724  omgadd  10782  reim0b  10871  rereb  10872  immul2  10889  resqrexlemcalc3  11025  resqrexlemnm  11027  max0addsup  11228  fsumsplit  11415  sumsplitdc  11440  bezoutlema  12000  pcadd  12339  pcmpt  12341  mulgnn0dir  13013  cosmpi  14240  sinppi  14241  sinhalfpip  14244  trilpolemlt1  14792