Theorem addridd 8168

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 8157	. 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 5918   CCcc 7870   0cc0 7872   + caddc 7875

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

This theorem is referenced by:  subsub2  8247  negsub  8267  ltaddneg  8443  ltaddpos  8471  addge01  8491  add20  8493  apreap  8606  nnge1  9005  nnnn0addcl  9270  un0addcl  9273  peano2z  9353  zaddcl  9357  uzaddcl  9651  xaddid1  9928  fzosubel3  10263  expadd  10652  faclbnd6  10815  omgadd  10873  reim0b  11006  rereb  11007  immul2  11024  resqrexlemcalc3  11160  resqrexlemnm  11162  max0addsup  11363  fsumsplit  11550  sumsplitdc  11575  bezoutlema  12136  pcadd  12478  pcadd2  12479  pcmpt  12481  mulgnn0dir  13222  cosmpi  14951  sinppi  14952  sinhalfpip  14955  trilpolemlt1  15531