Theorem addridd 8422

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   0cc0 8127   + caddc 8130

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

This theorem is referenced by:  subsub2  8501  negsub  8521  ltaddneg  8698  ltaddpos  8726  addge01  8746  add20  8748  apreap  8861  nnge1  9260  nnnn0addcl  9526  un0addcl  9529  peano2z  9613  zaddcl  9617  uzaddcl  9918  xaddid1  10195  fzosubel3  10541  expadd  10943  faclbnd6  11106  omgadd  11166  ccatrid  11295  pfxmpt  11372  pfxfv  11376  pfxswrd  11398  pfxccatin12lem1  11420  pfxccatin12lem2  11423  swrdccat3blem  11431  reim0b  11547  rereb  11548  immul2  11565  resqrexlemcalc3  11701  resqrexlemnm  11703  max0addsup  11904  fsumsplit  12093  sumsplitdc  12118  bitsinv1lem  12647  bezoutlema  12695  pcadd  13038  pcadd2  13039  pcmpt  13041  mulgnn0dir  13869  cosmpi  15681  sinppi  15682  sinhalfpip  15685  vtxdumgrfival  16293  p1evtxdeqfi  16307  eupth2lem3lem6fi  16466  trilpolemlt1  16825