Theorem addid1d 8003

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 2125  (class class class)co 5814   CCcc 7709   0cc0 7711   + caddc 7714

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

This theorem is referenced by:  subsub2  8082  negsub  8102  ltaddneg  8278  ltaddpos  8306  addge01  8326  add20  8328  apreap  8441  nnge1  8835  nnnn0addcl  9099  un0addcl  9102  peano2z  9182  zaddcl  9186  uzaddcl  9476  xaddid1  9744  fzosubel3  10073  expadd  10439  faclbnd6  10595  omgadd  10653  reim0b  10739  rereb  10740  immul2  10757  resqrexlemcalc3  10893  resqrexlemnm  10895  max0addsup  11096  fsumsplit  11281  sumsplitdc  11306  bezoutlema  11854  cosmpi  13076  sinppi  13077  sinhalfpip  13080  trilpolemlt1  13553