Theorem addridd 8192

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
addridd	|- ( ph -> ( A + 0 ) = A )

Proof of Theorem addridd

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addrid 8181	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( A + 0 ) = A )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   0cc0 7896   + caddc 7899

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

This theorem is referenced by:  subsub2  8271  negsub  8291  ltaddneg  8468  ltaddpos  8496  addge01  8516  add20  8518  apreap  8631  nnge1  9030  nnnn0addcl  9296  un0addcl  9299  peano2z  9379  zaddcl  9383  uzaddcl  9677  xaddid1  9954  fzosubel3  10289  expadd  10690  faclbnd6  10853  omgadd  10911  reim0b  11044  rereb  11045  immul2  11062  resqrexlemcalc3  11198  resqrexlemnm  11200  max0addsup  11401  fsumsplit  11589  sumsplitdc  11614  bitsinv1lem  12143  bezoutlema  12191  pcadd  12534  pcadd2  12535  pcmpt  12537  mulgnn0dir  13358  cosmpi  15136  sinppi  15137  sinhalfpip  15140  trilpolemlt1  15772