Theorem addridd 8333

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035  0cc0 8037   + caddc 8040

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

This theorem is referenced by:  subsub2  8412  negsub  8432  ltaddneg  8609  ltaddpos  8637  addge01  8657  add20  8659  apreap  8772  nnge1  9171  nnnn0addcl  9437  un0addcl  9440  peano2z  9520  zaddcl  9524  uzaddcl  9825  xaddid1  10102  fzosubel3  10447  expadd  10849  faclbnd6  11012  omgadd  11071  ccatrid  11193  pfxmpt  11270  pfxfv  11274  pfxswrd  11296  pfxccatin12lem1  11318  pfxccatin12lem2  11321  swrdccat3blem  11329  reim0b  11445  rereb  11446  immul2  11463  resqrexlemcalc3  11599  resqrexlemnm  11601  max0addsup  11802  fsumsplit  11991  sumsplitdc  12016  bitsinv1lem  12545  bezoutlema  12593  pcadd  12936  pcadd2  12937  pcmpt  12939  mulgnn0dir  13762  cosmpi  15569  sinppi  15570  sinhalfpip  15573  vtxdumgrfival  16178  p1evtxdeqfi  16192  eupth2lem3lem6fi  16351  trilpolemlt1  16712