Theorem addridd 8328

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030  0cc0 8032   + caddc 8035

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

This theorem is referenced by:  subsub2  8407  negsub  8427  ltaddneg  8604  ltaddpos  8632  addge01  8652  add20  8654  apreap  8767  nnge1  9166  nnnn0addcl  9432  un0addcl  9435  peano2z  9515  zaddcl  9519  uzaddcl  9820  xaddid1  10097  fzosubel3  10442  expadd  10844  faclbnd6  11007  omgadd  11066  ccatrid  11185  pfxmpt  11262  pfxfv  11266  pfxswrd  11288  pfxccatin12lem1  11310  pfxccatin12lem2  11313  swrdccat3blem  11321  reim0b  11424  rereb  11425  immul2  11442  resqrexlemcalc3  11578  resqrexlemnm  11580  max0addsup  11781  fsumsplit  11970  sumsplitdc  11995  bitsinv1lem  12524  bezoutlema  12572  pcadd  12915  pcadd2  12916  pcmpt  12918  mulgnn0dir  13741  cosmpi  15543  sinppi  15544  sinhalfpip  15547  vtxdumgrfival  16152  p1evtxdeqfi  16166  eupth2lem3lem6fi  16325  trilpolemlt1  16666