Theorem addridd 8477

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   0cc0 8180   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 8288

This theorem is used by:  subsub2  8556  negsub  8576  ltaddneg  8754  ltaddpos  8782  addge01  8802  add20  8804  apreap  8918  nnge1  9330  nnnn0addcl  9598  un0addcl  9601  peano2z  9685  zaddcl  9689  uzaddcl  9996  xaddid1  10275  fzosubel3  10625  expadd  11033  faclbnd6  11198  omgadd  11258  ccatrid  11391  pfxmpt  11468  pfxfv  11472  pfxswrd  11494  pfxccatin12lem1  11516  pfxccatin12lem2  11519  swrdccat3blem  11527  reim0b  11643  rereb  11644  immul2  11661  resqrexlemcalc3  11798  resqrexlemnm  11800  max0addsup  12002  fsumsplit  12193  sumsplitdc  12218  bitsinv1lem  12747  bezoutlema  12795  pcadd  13142  pcadd2  13143  pcmpt  13145  mulgnn0dir  14008  cosmpi  16009  sinppi  16010  sinhalfpip  16013  zprmlogbaplem2  16177  vtxdumgrfival  16705  p1evtxdeqfi  16719  eupth2lem3lem6fi  16878  trilpolemlt1  17257