Theorem addid1d 8068

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   0cc0 7774   + caddc 7777

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

This theorem is referenced by:  subsub2  8147  negsub  8167  ltaddneg  8343  ltaddpos  8371  addge01  8391  add20  8393  apreap  8506  nnge1  8901  nnnn0addcl  9165  un0addcl  9168  peano2z  9248  zaddcl  9252  uzaddcl  9545  xaddid1  9819  fzosubel3  10152  expadd  10518  faclbnd6  10678  omgadd  10737  reim0b  10826  rereb  10827  immul2  10844  resqrexlemcalc3  10980  resqrexlemnm  10982  max0addsup  11183  fsumsplit  11370  sumsplitdc  11395  bezoutlema  11954  pcadd  12293  pcmpt  12295  cosmpi  13531  sinppi  13532  sinhalfpip  13535  trilpolemlt1  14073