Theorem addid1d 8108

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
addid1d	|- ( ph -> ( A + 0 ) = A )

Proof of Theorem addid1d

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addid1 8097	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( A + 0 ) = A )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   0cc0 7813   + caddc 7816

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

This theorem is referenced by:  subsub2  8187  negsub  8207  ltaddneg  8383  ltaddpos  8411  addge01  8431  add20  8433  apreap  8546  nnge1  8944  nnnn0addcl  9208  un0addcl  9211  peano2z  9291  zaddcl  9295  uzaddcl  9588  xaddid1  9864  fzosubel3  10198  expadd  10564  faclbnd6  10726  omgadd  10784  reim0b  10873  rereb  10874  immul2  10891  resqrexlemcalc3  11027  resqrexlemnm  11029  max0addsup  11230  fsumsplit  11417  sumsplitdc  11442  bezoutlema  12002  pcadd  12341  pcmpt  12343  mulgnn0dir  13018  cosmpi  14322  sinppi  14323  sinhalfpip  14326  trilpolemlt1  14874