Theorem addridd 8370

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 8359	. 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 2202  (class class class)co 6028   CCcc 8073   0cc0 8075   + caddc 8078

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

This theorem is referenced by:  subsub2  8449  negsub  8469  ltaddneg  8646  ltaddpos  8674  addge01  8694  add20  8696  apreap  8809  nnge1  9208  nnnn0addcl  9474  un0addcl  9477  peano2z  9559  zaddcl  9563  uzaddcl  9864  xaddid1  10141  fzosubel3  10487  expadd  10889  faclbnd6  11052  omgadd  11111  ccatrid  11233  pfxmpt  11310  pfxfv  11314  pfxswrd  11336  pfxccatin12lem1  11358  pfxccatin12lem2  11361  swrdccat3blem  11369  reim0b  11485  rereb  11486  immul2  11503  resqrexlemcalc3  11639  resqrexlemnm  11641  max0addsup  11842  fsumsplit  12031  sumsplitdc  12056  bitsinv1lem  12585  bezoutlema  12633  pcadd  12976  pcadd2  12977  pcmpt  12979  mulgnn0dir  13802  cosmpi  15610  sinppi  15611  sinhalfpip  15614  vtxdumgrfival  16222  p1evtxdeqfi  16236  eupth2lem3lem6fi  16395  trilpolemlt1  16756