Theorem addridd 8175

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 8164	. 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 2167  (class class class)co 5922   CCcc 7877   0cc0 7879   + caddc 7882

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

This theorem is referenced by:  subsub2  8254  negsub  8274  ltaddneg  8451  ltaddpos  8479  addge01  8499  add20  8501  apreap  8614  nnge1  9013  nnnn0addcl  9279  un0addcl  9282  peano2z  9362  zaddcl  9366  uzaddcl  9660  xaddid1  9937  fzosubel3  10272  expadd  10673  faclbnd6  10836  omgadd  10894  reim0b  11027  rereb  11028  immul2  11045  resqrexlemcalc3  11181  resqrexlemnm  11183  max0addsup  11384  fsumsplit  11572  sumsplitdc  11597  bezoutlema  12166  pcadd  12509  pcadd2  12510  pcmpt  12512  mulgnn0dir  13282  cosmpi  15052  sinppi  15053  sinhalfpip  15056  trilpolemlt1  15685