Theorem addridd 8311

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013  0cc0 8015   + caddc 8018

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

This theorem is referenced by:  subsub2  8390  negsub  8410  ltaddneg  8587  ltaddpos  8615  addge01  8635  add20  8637  apreap  8750  nnge1  9149  nnnn0addcl  9415  un0addcl  9418  peano2z  9498  zaddcl  9502  uzaddcl  9798  xaddid1  10075  fzosubel3  10419  expadd  10820  faclbnd6  10983  omgadd  11041  ccatrid  11160  pfxmpt  11233  pfxfv  11237  pfxswrd  11259  pfxccatin12lem1  11281  pfxccatin12lem2  11284  swrdccat3blem  11292  reim0b  11394  rereb  11395  immul2  11412  resqrexlemcalc3  11548  resqrexlemnm  11550  max0addsup  11751  fsumsplit  11939  sumsplitdc  11964  bitsinv1lem  12493  bezoutlema  12541  pcadd  12884  pcadd2  12885  pcmpt  12887  mulgnn0dir  13710  cosmpi  15511  sinppi  15512  sinhalfpip  15515  vtxdumgrfival  16084  trilpolemlt1  16523