Theorem addridd 8465

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

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   0cc0 8169   + caddc 8172

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

This theorem is referenced by:  subsub2  8544  negsub  8564  ltaddneg  8742  ltaddpos  8770  addge01  8790  add20  8792  apreap  8905  nnge1  9306  nnnn0addcl  9572  un0addcl  9575  peano2z  9659  zaddcl  9663  uzaddcl  9965  xaddid1  10243  fzosubel3  10592  expadd  10996  faclbnd6  11160  omgadd  11220  ccatrid  11353  pfxmpt  11430  pfxfv  11434  pfxswrd  11456  pfxccatin12lem1  11478  pfxccatin12lem2  11481  swrdccat3blem  11489  reim0b  11605  rereb  11606  immul2  11623  resqrexlemcalc3  11760  resqrexlemnm  11762  max0addsup  11963  fsumsplit  12152  sumsplitdc  12177  bitsinv1lem  12706  bezoutlema  12754  pcadd  13097  pcadd2  13098  pcmpt  13100  mulgnn0dir  13932  cosmpi  15840  sinppi  15841  sinhalfpip  15844  vtxdumgrfival  16453  p1evtxdeqfi  16467  eupth2lem3lem6fi  16626  trilpolemlt1  16995