Theorem addridd 8475

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 8464	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( A + 0 ) = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 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  8915  nnge1  9327  nnnn0addcl  9593  un0addcl  9596  peano2z  9680  zaddcl  9684  uzaddcl  9986  xaddid1  10264  fzosubel3  10614  expadd  11018  faclbnd6  11182  omgadd  11242  ccatrid  11375  pfxmpt  11452  pfxfv  11456  pfxswrd  11478  pfxccatin12lem1  11500  pfxccatin12lem2  11503  swrdccat3blem  11511  reim0b  11627  rereb  11628  immul2  11645  resqrexlemcalc3  11782  resqrexlemnm  11784  max0addsup  11985  fsumsplit  12174  sumsplitdc  12199  bitsinv1lem  12728  bezoutlema  12776  pcadd  13119  pcadd2  13120  pcmpt  13122  mulgnn0dir  13955  cosmpi  15917  sinppi  15918  sinhalfpip  15921  vtxdumgrfival  16539  p1evtxdeqfi  16553  eupth2lem3lem6fi  16712  trilpolemlt1  17090