Theorem addridd 8482

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   0cc0 8185   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 8293

This theorem is used by:  subsub2  8561  negsub  8581  ltaddneg  8759  ltaddpos  8787  addge01  8807  add20  8809  apreap  8923  nnge1  9336  nnnn0addcl  9604  un0addcl  9607  peano2z  9689  zaddcl  9693  uzaddcl  10001  xaddid1  10280  fzosubel3  10630  expadd  11038  faclbnd6  11203  omgadd  11263  ccatrid  11396  pfxmpt  11473  pfxfv  11477  pfxswrd  11499  pfxccatin12lem1  11521  pfxccatin12lem2  11524  swrdccat3blem  11532  reim0b  11648  rereb  11649  immul2  11666  resqrexlemcalc3  11803  resqrexlemnm  11805  max0addsup  12007  fsumsplit  12198  sumsplitdc  12223  bitsinv1lem  12752  bezoutlema  12800  pcadd  13147  pcadd2  13148  pcmpt  13150  mulgnn0dir  14013  cosmpi  16060  sinppi  16061  sinhalfpip  16064  zprmlogbaplem2  16233  vtxdumgrfival  16761  p1evtxdeqfi  16775  eupth2lem3lem6fi  16934  trilpolemlt1  17314