Theorem addridd 8427

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130  0cc0 8132   + caddc 8135

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

This theorem is referenced by:  subsub2  8506  negsub  8526  ltaddneg  8703  ltaddpos  8731  addge01  8751  add20  8753  apreap  8866  nnge1  9265  nnnn0addcl  9531  un0addcl  9534  peano2z  9618  zaddcl  9622  uzaddcl  9924  xaddid1  10201  fzosubel3  10548  expadd  10950  faclbnd6  11114  omgadd  11174  ccatrid  11303  pfxmpt  11380  pfxfv  11384  pfxswrd  11406  pfxccatin12lem1  11428  pfxccatin12lem2  11431  swrdccat3blem  11439  reim0b  11555  rereb  11556  immul2  11573  resqrexlemcalc3  11709  resqrexlemnm  11711  max0addsup  11912  fsumsplit  12101  sumsplitdc  12126  bitsinv1lem  12655  bezoutlema  12703  pcadd  13046  pcadd2  13047  pcmpt  13049  mulgnn0dir  13890  cosmpi  15730  sinppi  15731  sinhalfpip  15734  vtxdumgrfival  16342  p1evtxdeqfi  16356  eupth2lem3lem6fi  16515  trilpolemlt1  16874