Theorem addid1d 8047

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   0cc0 7753   + caddc 7756

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

This theorem is referenced by:  subsub2  8126  negsub  8146  ltaddneg  8322  ltaddpos  8350  addge01  8370  add20  8372  apreap  8485  nnge1  8880  nnnn0addcl  9144  un0addcl  9147  peano2z  9227  zaddcl  9231  uzaddcl  9524  xaddid1  9798  fzosubel3  10131  expadd  10497  faclbnd6  10657  omgadd  10715  reim0b  10804  rereb  10805  immul2  10822  resqrexlemcalc3  10958  resqrexlemnm  10960  max0addsup  11161  fsumsplit  11348  sumsplitdc  11373  bezoutlema  11932  pcadd  12271  pcmpt  12273  cosmpi  13377  sinppi  13378  sinhalfpip  13381  trilpolemlt1  13920