Theorem addid1d 8100

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 8089	. 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 5870   CCcc 7804   0cc0 7806   + caddc 7809

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

This theorem is referenced by:  subsub2  8179  negsub  8199  ltaddneg  8375  ltaddpos  8403  addge01  8423  add20  8425  apreap  8538  nnge1  8936  nnnn0addcl  9200  un0addcl  9203  peano2z  9283  zaddcl  9287  uzaddcl  9580  xaddid1  9856  fzosubel3  10189  expadd  10555  faclbnd6  10715  omgadd  10773  reim0b  10862  rereb  10863  immul2  10880  resqrexlemcalc3  11016  resqrexlemnm  11018  max0addsup  11219  fsumsplit  11406  sumsplitdc  11431  bezoutlema  11990  pcadd  12329  pcmpt  12331  mulgnn0dir  12940  cosmpi  14019  sinppi  14020  sinhalfpip  14023  trilpolemlt1  14560