Theorem addridd 8194

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

Hypothesis

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

Assertion

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

Proof of Theorem addridd

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896  0cc0 7898   + caddc 7901

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

This theorem is referenced by:  subsub2  8273  negsub  8293  ltaddneg  8470  ltaddpos  8498  addge01  8518  add20  8520  apreap  8633  nnge1  9032  nnnn0addcl  9298  un0addcl  9301  peano2z  9381  zaddcl  9385  uzaddcl  9679  xaddid1  9956  fzosubel3  10291  expadd  10692  faclbnd6  10855  omgadd  10913  reim0b  11046  rereb  11047  immul2  11064  resqrexlemcalc3  11200  resqrexlemnm  11202  max0addsup  11403  fsumsplit  11591  sumsplitdc  11616  bitsinv1lem  12145  bezoutlema  12193  pcadd  12536  pcadd2  12537  pcmpt  12539  mulgnn0dir  13360  cosmpi  15138  sinppi  15139  sinhalfpip  15142  trilpolemlt1  15776