Theorem addlidd 8169

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5918   CCcc 7870   0cc0 7872   + caddc 7875

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-addcom 7972  ax-i2m1 7977  ax-0id 7980

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  negeu  8210  ltadd2  8438  subge0  8494  sublt0d  8589  un0addcl  9273  lincmb01cmp  10069  modsumfzodifsn  10467  rennim  11146  max0addsup  11363  fsumsplit  11550  sumsplitdc  11575  fisum0diag2  11590  isumsplit  11634  arisum2  11642  efaddlem  11817  eftlub  11833  ef4p  11837  moddvds  11942  gcdaddm  12121  gcdmultipled  12130  bezoutlemb  12137  pcmpt  12481  4sqlem11  12539  mulgnn0dir  13222  limcimolemlt  14818  dvcnp2cntop  14848  dvmptcmulcn  14868  dveflem  14872  dvef  14873  plymullem1  14894  sin0pilem1  14916  sin2kpi  14946  cos2kpi  14947  coshalfpim  14958  sinkpi  14982