Theorem addid1d 7834

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

Syntax hints:   -> wi 4   = wceq 1314   e. wcel 1463  (class class class)co 5728   CCcc 7545   0cc0 7547   + caddc 7550

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

This theorem is referenced by:  subsub2  7913  negsub  7933  ltaddneg  8105  ltaddpos  8133  addge01  8153  add20  8155  apreap  8267  nnge1  8653  nnnn0addcl  8911  un0addcl  8914  peano2z  8994  zaddcl  8998  uzaddcl  9283  xaddid1  9538  fzosubel3  9866  expadd  10228  faclbnd6  10383  omgadd  10441  reim0b  10527  rereb  10528  immul2  10545  resqrexlemcalc3  10680  resqrexlemnm  10682  max0addsup  10883  fsumsplit  11068  sumsplitdc  11093  bezoutlema  11533  trilpolemlt1  12926