Theorem addridd 8330

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
addridd	|- ( ph -> ( A + 0 ) = A )

Proof of Theorem addridd

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addrid 8319	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( A + 0 ) = A )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2201  (class class class)co 6020   CCcc 8032   0cc0 8034   + caddc 8037

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

This theorem is referenced by:  subsub2  8409  negsub  8429  ltaddneg  8606  ltaddpos  8634  addge01  8654  add20  8656  apreap  8769  nnge1  9168  nnnn0addcl  9434  un0addcl  9437  peano2z  9517  zaddcl  9521  uzaddcl  9822  xaddid1  10099  fzosubel3  10444  expadd  10846  faclbnd6  11009  omgadd  11068  ccatrid  11190  pfxmpt  11267  pfxfv  11271  pfxswrd  11293  pfxccatin12lem1  11315  pfxccatin12lem2  11318  swrdccat3blem  11326  reim0b  11442  rereb  11443  immul2  11460  resqrexlemcalc3  11596  resqrexlemnm  11598  max0addsup  11799  fsumsplit  11988  sumsplitdc  12013  bitsinv1lem  12542  bezoutlema  12590  pcadd  12933  pcadd2  12934  pcmpt  12936  mulgnn0dir  13759  cosmpi  15566  sinppi  15567  sinhalfpip  15570  vtxdumgrfival  16175  p1evtxdeqfi  16189  eupth2lem3lem6fi  16348  trilpolemlt1  16707