Theorem addridd 8321

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023  0cc0 8025   + caddc 8028

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

This theorem is referenced by:  subsub2  8400  negsub  8420  ltaddneg  8597  ltaddpos  8625  addge01  8645  add20  8647  apreap  8760  nnge1  9159  nnnn0addcl  9425  un0addcl  9428  peano2z  9508  zaddcl  9512  uzaddcl  9813  xaddid1  10090  fzosubel3  10434  expadd  10836  faclbnd6  10999  omgadd  11058  ccatrid  11177  pfxmpt  11254  pfxfv  11258  pfxswrd  11280  pfxccatin12lem1  11302  pfxccatin12lem2  11305  swrdccat3blem  11313  reim0b  11416  rereb  11417  immul2  11434  resqrexlemcalc3  11570  resqrexlemnm  11572  max0addsup  11773  fsumsplit  11961  sumsplitdc  11986  bitsinv1lem  12515  bezoutlema  12563  pcadd  12906  pcadd2  12907  pcmpt  12909  mulgnn0dir  13732  cosmpi  15533  sinppi  15534  sinhalfpip  15537  vtxdumgrfival  16109  p1evtxdeqfi  16123  trilpolemlt1  16595