Theorem addridd 8203

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

Syntax hints:   -> wi 4   = wceq 1372   e. wcel 2175  (class class class)co 5934   CCcc 7905   0cc0 7907   + caddc 7910

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

This theorem is referenced by:  subsub2  8282  negsub  8302  ltaddneg  8479  ltaddpos  8507  addge01  8527  add20  8529  apreap  8642  nnge1  9041  nnnn0addcl  9307  un0addcl  9310  peano2z  9390  zaddcl  9394  uzaddcl  9689  xaddid1  9966  fzosubel3  10306  expadd  10707  faclbnd6  10870  omgadd  10928  ccatrid  11038  reim0b  11092  rereb  11093  immul2  11110  resqrexlemcalc3  11246  resqrexlemnm  11248  max0addsup  11449  fsumsplit  11637  sumsplitdc  11662  bitsinv1lem  12191  bezoutlema  12239  pcadd  12582  pcadd2  12583  pcmpt  12585  mulgnn0dir  13406  cosmpi  15206  sinppi  15207  sinhalfpip  15210  trilpolemlt1  15844