Theorem addridd 8137

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 8126	. 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 2160  (class class class)co 5897   CCcc 7840   0cc0 7842   + caddc 7845

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

This theorem is referenced by:  subsub2  8216  negsub  8236  ltaddneg  8412  ltaddpos  8440  addge01  8460  add20  8462  apreap  8575  nnge1  8973  nnnn0addcl  9237  un0addcl  9240  peano2z  9320  zaddcl  9324  uzaddcl  9618  xaddid1  9894  fzosubel3  10228  expadd  10596  faclbnd6  10759  omgadd  10817  reim0b  10906  rereb  10907  immul2  10924  resqrexlemcalc3  11060  resqrexlemnm  11062  max0addsup  11263  fsumsplit  11450  sumsplitdc  11475  bezoutlema  12035  pcadd  12375  pcadd2  12376  pcmpt  12378  mulgnn0dir  13109  cosmpi  14714  sinppi  14715  sinhalfpip  14718  trilpolemlt1  15268