Theorem addridd 8439

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141  0cc0 8143   + caddc 8146

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

This theorem is referenced by:  subsub2  8518  negsub  8538  ltaddneg  8716  ltaddpos  8744  addge01  8764  add20  8766  apreap  8879  nnge1  9280  nnnn0addcl  9546  un0addcl  9549  peano2z  9633  zaddcl  9637  uzaddcl  9939  xaddid1  10217  fzosubel3  10566  expadd  10970  faclbnd6  11134  omgadd  11194  ccatrid  11323  pfxmpt  11400  pfxfv  11404  pfxswrd  11426  pfxccatin12lem1  11448  pfxccatin12lem2  11451  swrdccat3blem  11459  reim0b  11575  rereb  11576  immul2  11593  resqrexlemcalc3  11729  resqrexlemnm  11731  max0addsup  11932  fsumsplit  12121  sumsplitdc  12146  bitsinv1lem  12675  bezoutlema  12723  pcadd  13066  pcadd2  13067  pcmpt  13069  mulgnn0dir  13908  cosmpi  15810  sinppi  15811  sinhalfpip  15814  vtxdumgrfival  16422  p1evtxdeqfi  16436  eupth2lem3lem6fi  16595  trilpolemlt1  16964