Theorem addridd 8475

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  0cc0 8179   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 8287

This theorem is used by:  subsub2  8554  negsub  8574  ltaddneg  8752  ltaddpos  8780  addge01  8800  add20  8802  apreap  8916  nnge1  9328  nnnn0addcl  9595  un0addcl  9598  peano2z  9682  zaddcl  9686  uzaddcl  9988  xaddid1  10266  fzosubel3  10616  expadd  11020  faclbnd6  11184  omgadd  11244  ccatrid  11377  pfxmpt  11454  pfxfv  11458  pfxswrd  11480  pfxccatin12lem1  11502  pfxccatin12lem2  11505  swrdccat3blem  11513  reim0b  11629  rereb  11630  immul2  11647  resqrexlemcalc3  11784  resqrexlemnm  11786  max0addsup  11987  fsumsplit  12176  sumsplitdc  12201  bitsinv1lem  12730  bezoutlema  12778  pcadd  13121  pcadd2  13122  pcmpt  13124  mulgnn0dir  13957  cosmpi  15920  sinppi  15921  sinhalfpip  15924  vtxdumgrfival  16551  p1evtxdeqfi  16565  eupth2lem3lem6fi  16724  trilpolemlt1  17102