Theorem addid1d 8109

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 8098	. 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 5878   CCcc 7812   0cc0 7814   + caddc 7817

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

This theorem is referenced by:  subsub2  8188  negsub  8208  ltaddneg  8384  ltaddpos  8412  addge01  8432  add20  8434  apreap  8547  nnge1  8945  nnnn0addcl  9209  un0addcl  9212  peano2z  9292  zaddcl  9296  uzaddcl  9589  xaddid1  9865  fzosubel3  10199  expadd  10565  faclbnd6  10727  omgadd  10785  reim0b  10874  rereb  10875  immul2  10892  resqrexlemcalc3  11028  resqrexlemnm  11030  max0addsup  11231  fsumsplit  11418  sumsplitdc  11443  bezoutlema  12003  pcadd  12342  pcmpt  12344  mulgnn0dir  13019  cosmpi  14377  sinppi  14378  sinhalfpip  14381  trilpolemlt1  14929