Theorem addridd 8328

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 8317	. 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 6018   CCcc 8030   0cc0 8032   + caddc 8035

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

This theorem is referenced by:  subsub2  8407  negsub  8427  ltaddneg  8604  ltaddpos  8632  addge01  8652  add20  8654  apreap  8767  nnge1  9166  nnnn0addcl  9432  un0addcl  9435  peano2z  9515  zaddcl  9519  uzaddcl  9820  xaddid1  10097  fzosubel3  10442  expadd  10844  faclbnd6  11007  omgadd  11066  ccatrid  11188  pfxmpt  11265  pfxfv  11269  pfxswrd  11291  pfxccatin12lem1  11313  pfxccatin12lem2  11316  swrdccat3blem  11324  reim0b  11440  rereb  11441  immul2  11458  resqrexlemcalc3  11594  resqrexlemnm  11596  max0addsup  11797  fsumsplit  11986  sumsplitdc  12011  bitsinv1lem  12540  bezoutlema  12588  pcadd  12931  pcadd2  12932  pcmpt  12934  mulgnn0dir  13757  cosmpi  15559  sinppi  15560  sinhalfpip  15563  vtxdumgrfival  16168  p1evtxdeqfi  16182  eupth2lem3lem6fi  16341  trilpolemlt1  16696