Theorem addridd 8177

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167  (class class class)co 5923   CCcc 7879   0cc0 7881   + caddc 7884

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

This theorem is referenced by:  subsub2  8256  negsub  8276  ltaddneg  8453  ltaddpos  8481  addge01  8501  add20  8503  apreap  8616  nnge1  9015  nnnn0addcl  9281  un0addcl  9284  peano2z  9364  zaddcl  9368  uzaddcl  9662  xaddid1  9939  fzosubel3  10274  expadd  10675  faclbnd6  10838  omgadd  10896  reim0b  11029  rereb  11030  immul2  11047  resqrexlemcalc3  11183  resqrexlemnm  11185  max0addsup  11386  fsumsplit  11574  sumsplitdc  11599  bitsinv1lem  12128  bezoutlema  12176  pcadd  12519  pcadd2  12520  pcmpt  12522  mulgnn0dir  13292  cosmpi  15062  sinppi  15063  sinhalfpip  15066  trilpolemlt1  15695