Theorem addridd 8291

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   0cc0 7995   + caddc 7998

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

This theorem is referenced by:  subsub2  8370  negsub  8390  ltaddneg  8567  ltaddpos  8595  addge01  8615  add20  8617  apreap  8730  nnge1  9129  nnnn0addcl  9395  un0addcl  9398  peano2z  9478  zaddcl  9482  uzaddcl  9777  xaddid1  10054  fzosubel3  10397  expadd  10798  faclbnd6  10961  omgadd  11019  ccatrid  11137  pfxmpt  11207  pfxfv  11211  pfxswrd  11233  pfxccatin12lem1  11255  pfxccatin12lem2  11258  swrdccat3blem  11266  reim0b  11368  rereb  11369  immul2  11386  resqrexlemcalc3  11522  resqrexlemnm  11524  max0addsup  11725  fsumsplit  11913  sumsplitdc  11938  bitsinv1lem  12467  bezoutlema  12515  pcadd  12858  pcadd2  12859  pcmpt  12861  mulgnn0dir  13684  cosmpi  15484  sinppi  15485  sinhalfpip  15488  trilpolemlt1  16368