Theorem addridd 8327

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 8316	. 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 2202  (class class class)co 6017   CCcc 8029   0cc0 8031   + caddc 8034

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

This theorem is referenced by:  subsub2  8406  negsub  8426  ltaddneg  8603  ltaddpos  8631  addge01  8651  add20  8653  apreap  8766  nnge1  9165  nnnn0addcl  9431  un0addcl  9434  peano2z  9514  zaddcl  9518  uzaddcl  9819  xaddid1  10096  fzosubel3  10440  expadd  10842  faclbnd6  11005  omgadd  11064  ccatrid  11183  pfxmpt  11260  pfxfv  11264  pfxswrd  11286  pfxccatin12lem1  11308  pfxccatin12lem2  11311  swrdccat3blem  11319  reim0b  11422  rereb  11423  immul2  11440  resqrexlemcalc3  11576  resqrexlemnm  11578  max0addsup  11779  fsumsplit  11967  sumsplitdc  11992  bitsinv1lem  12521  bezoutlema  12569  pcadd  12912  pcadd2  12913  pcmpt  12915  mulgnn0dir  13738  cosmpi  15539  sinppi  15540  sinhalfpip  15543  vtxdumgrfival  16148  p1evtxdeqfi  16162  trilpolemlt1  16645