Theorem addlidd 8478

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-addcom 8280  ax-i2m1 8285  ax-0id 8288

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  negeu  8519  ltadd2  8749  subge0  8805  sublt0d  8901  un0addcl  9601  lincmb01cmp  10416  modsumfzodifsn  10848  bcm1n  11223  ccatlid  11390  swrdfv0  11442  swrdpfx  11495  pfxpfx  11496  cats1un  11509  swrdccatin2  11517  cats1fvnd  11553  rennim  11784  max0addsup  12002  fsumsplit  12193  sumsplitdc  12218  fisum0diag2  12233  isumsplit  12277  arisum2  12285  efaddlem  12460  eftlub  12476  ef4p  12480  moddvds  12585  gcdaddm  12780  gcdmultipled  12789  bezoutlemb  12796  pcmpt  13145  4sqlem11  13203  mulgnn0dir  14007  limcimolemlt  15824  dvcnp2cntop  15859  dvmptcmulcn  15881  dveflem  15886  dvef  15887  plymullem1  15908  sin0pilem1  15942  sin2kpi  15972  cos2kpi  15973  coshalfpim  15984  sinkpi  16008  logfac  16058  chtublem  16224