Theorem addridd 8469

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 8458	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171  0cc0 8173   + caddc 8176

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

This theorem is referenced by:  subsub2  8548  negsub  8568  ltaddneg  8746  ltaddpos  8774  addge01  8794  add20  8796  apreap  8909  nnge1  9310  nnnn0addcl  9576  un0addcl  9579  peano2z  9663  zaddcl  9667  uzaddcl  9969  xaddid1  10247  fzosubel3  10597  expadd  11001  faclbnd6  11165  omgadd  11225  ccatrid  11358  pfxmpt  11435  pfxfv  11439  pfxswrd  11461  pfxccatin12lem1  11483  pfxccatin12lem2  11486  swrdccat3blem  11494  reim0b  11610  rereb  11611  immul2  11628  resqrexlemcalc3  11765  resqrexlemnm  11767  max0addsup  11968  fsumsplit  12157  sumsplitdc  12182  bitsinv1lem  12711  bezoutlema  12759  pcadd  13102  pcadd2  13103  pcmpt  13105  mulgnn0dir  13938  cosmpi  15900  sinppi  15901  sinhalfpip  15904  vtxdumgrfival  16522  p1evtxdeqfi  16536  eupth2lem3lem6fi  16695  trilpolemlt1  17064