Theorem addridd 8438

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

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

This theorem is referenced by:  subsub2  8517  negsub  8537  ltaddneg  8715  ltaddpos  8743  addge01  8763  add20  8765  apreap  8878  nnge1  9277  nnnn0addcl  9543  un0addcl  9546  peano2z  9630  zaddcl  9634  uzaddcl  9936  xaddid1  10214  fzosubel3  10563  expadd  10967  faclbnd6  11131  omgadd  11191  ccatrid  11320  pfxmpt  11397  pfxfv  11401  pfxswrd  11423  pfxccatin12lem1  11445  pfxccatin12lem2  11448  swrdccat3blem  11456  reim0b  11572  rereb  11573  immul2  11590  resqrexlemcalc3  11726  resqrexlemnm  11728  max0addsup  11929  fsumsplit  12118  sumsplitdc  12143  bitsinv1lem  12672  bezoutlema  12720  pcadd  13063  pcadd2  13064  pcmpt  13066  mulgnn0dir  13905  cosmpi  15807  sinppi  15808  sinhalfpip  15811  vtxdumgrfival  16419  p1evtxdeqfi  16433  eupth2lem3lem6fi  16592  trilpolemlt1  16951