Theorem addridd 8476

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 8465	. 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 8177   0cc0 8179   + caddc 8182

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

This theorem is used by:  subsub2  8555  negsub  8575  ltaddneg  8753  ltaddpos  8781  addge01  8801  add20  8803  apreap  8917  nnge1  9329  nnnn0addcl  9597  un0addcl  9600  peano2z  9684  zaddcl  9688  uzaddcl  9995  xaddid1  10274  fzosubel3  10624  expadd  11031  faclbnd6  11196  omgadd  11256  ccatrid  11389  pfxmpt  11466  pfxfv  11470  pfxswrd  11492  pfxccatin12lem1  11514  pfxccatin12lem2  11517  swrdccat3blem  11525  reim0b  11641  rereb  11642  immul2  11659  resqrexlemcalc3  11796  resqrexlemnm  11798  max0addsup  12000  fsumsplit  12190  sumsplitdc  12215  bitsinv1lem  12744  bezoutlema  12792  pcadd  13139  pcadd2  13140  pcmpt  13142  mulgnn0dir  14004  cosmpi  15967  sinppi  15968  sinhalfpip  15971  zprmlogbaplem2  16135  vtxdumgrfival  16637  p1evtxdeqfi  16651  eupth2lem3lem6fi  16810  trilpolemlt1  17188