Theorem addridd 8170

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5919   CCcc 7872   0cc0 7874   + caddc 7877

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

This theorem is referenced by:  subsub2  8249  negsub  8269  ltaddneg  8445  ltaddpos  8473  addge01  8493  add20  8495  apreap  8608  nnge1  9007  nnnn0addcl  9273  un0addcl  9276  peano2z  9356  zaddcl  9360  uzaddcl  9654  xaddid1  9931  fzosubel3  10266  expadd  10655  faclbnd6  10818  omgadd  10876  reim0b  11009  rereb  11010  immul2  11027  resqrexlemcalc3  11163  resqrexlemnm  11165  max0addsup  11366  fsumsplit  11553  sumsplitdc  11578  bezoutlema  12139  pcadd  12481  pcadd2  12482  pcmpt  12484  mulgnn0dir  13225  cosmpi  14992  sinppi  14993  sinhalfpip  14996  trilpolemlt1  15601