Theorem addridd 8318

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8020   0cc0 8022   + caddc 8025

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

This theorem is referenced by:  subsub2  8397  negsub  8417  ltaddneg  8594  ltaddpos  8622  addge01  8642  add20  8644  apreap  8757  nnge1  9156  nnnn0addcl  9422  un0addcl  9425  peano2z  9505  zaddcl  9509  uzaddcl  9810  xaddid1  10087  fzosubel3  10431  expadd  10833  faclbnd6  10996  omgadd  11055  ccatrid  11174  pfxmpt  11251  pfxfv  11255  pfxswrd  11277  pfxccatin12lem1  11299  pfxccatin12lem2  11302  swrdccat3blem  11310  reim0b  11413  rereb  11414  immul2  11431  resqrexlemcalc3  11567  resqrexlemnm  11569  max0addsup  11770  fsumsplit  11958  sumsplitdc  11983  bitsinv1lem  12512  bezoutlema  12560  pcadd  12903  pcadd2  12904  pcmpt  12906  mulgnn0dir  13729  cosmpi  15530  sinppi  15531  sinhalfpip  15534  vtxdumgrfival  16104  trilpolemlt1  16581