Theorem addlidd 8440

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
addlidd	|- ( ph -> ( 0 + A ) = A )

Proof of Theorem addlidd

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  negeu  8481  ltadd2  8711  subge0  8767  sublt0d  8862  un0addcl  9549  lincmb01cmp  10358  modsumfzodifsn  10785  bcm1n  11159  ccatlid  11322  swrdfv0  11374  swrdpfx  11427  pfxpfx  11428  cats1un  11441  swrdccatin2  11449  cats1fvnd  11485  rennim  11716  max0addsup  11933  fsumsplit  12122  sumsplitdc  12147  fisum0diag2  12162  isumsplit  12206  arisum2  12214  efaddlem  12389  eftlub  12405  ef4p  12409  moddvds  12514  gcdaddm  12709  gcdmultipled  12718  bezoutlemb  12725  pcmpt  13070  4sqlem11  13128  mulgnn0dir  13909  limcimolemlt  15659  dvcnp2cntop  15694  dvmptcmulcn  15716  dveflem  15721  dvef  15722  plymullem1  15743  sin0pilem1  15776  sin2kpi  15806  cos2kpi  15807  coshalfpim  15818  sinkpi  15842