Theorem addridd 8482

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 8471	. 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 6088   CCcc 8183   0cc0 8185   + caddc 8188

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

This theorem is used by:  subsub2  8561  negsub  8581  ltaddneg  8759  ltaddpos  8787  addge01  8807  add20  8809  apreap  8923  nnge1  9336  nnnn0addcl  9604  un0addcl  9607  peano2z  9691  zaddcl  9695  uzaddcl  10002  xaddid1  10281  fzosubel3  10631  expadd  11039  faclbnd6  11204  omgadd  11264  ccatrid  11397  pfxmpt  11474  pfxfv  11478  pfxswrd  11500  pfxccatin12lem1  11522  pfxccatin12lem2  11525  swrdccat3blem  11533  reim0b  11649  rereb  11650  immul2  11667  resqrexlemcalc3  11804  resqrexlemnm  11806  max0addsup  12008  fsumsplit  12199  sumsplitdc  12224  bitsinv1lem  12753  bezoutlema  12801  pcadd  13148  pcadd2  13149  pcmpt  13151  mulgnn0dir  14014  cosmpi  16043  sinppi  16044  sinhalfpip  16047  zprmlogbaplem2  16216  vtxdumgrfival  16744  p1evtxdeqfi  16758  eupth2lem3lem6fi  16917  trilpolemlt1  17297