Theorem addridd 8306

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 8295	. 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 6007   CCcc 8008   0cc0 8010   + caddc 8013

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

This theorem is referenced by:  subsub2  8385  negsub  8405  ltaddneg  8582  ltaddpos  8610  addge01  8630  add20  8632  apreap  8745  nnge1  9144  nnnn0addcl  9410  un0addcl  9413  peano2z  9493  zaddcl  9497  uzaddcl  9793  xaddid1  10070  fzosubel3  10414  expadd  10815  faclbnd6  10978  omgadd  11036  ccatrid  11155  pfxmpt  11227  pfxfv  11231  pfxswrd  11253  pfxccatin12lem1  11275  pfxccatin12lem2  11278  swrdccat3blem  11286  reim0b  11388  rereb  11389  immul2  11406  resqrexlemcalc3  11542  resqrexlemnm  11544  max0addsup  11745  fsumsplit  11933  sumsplitdc  11958  bitsinv1lem  12487  bezoutlema  12535  pcadd  12878  pcadd2  12879  pcmpt  12881  mulgnn0dir  13704  cosmpi  15505  sinppi  15506  sinhalfpip  15509  vtxdumgrfival  16057  trilpolemlt1  16469