Theorem addlidd 8257

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178  (class class class)co 5967   CCcc 7958   0cc0 7960   + caddc 7963

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-mulcl 8058  ax-addcom 8060  ax-i2m1 8065  ax-0id 8068

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  negeu  8298  ltadd2  8527  subge0  8583  sublt0d  8678  un0addcl  9363  lincmb01cmp  10160  modsumfzodifsn  10578  ccatlid  11100  swrdfv0  11145  swrdpfx  11198  pfxpfx  11199  cats1un  11212  swrdccatin2  11220  rennim  11428  max0addsup  11645  fsumsplit  11833  sumsplitdc  11858  fisum0diag2  11873  isumsplit  11917  arisum2  11925  efaddlem  12100  eftlub  12116  ef4p  12120  moddvds  12225  gcdaddm  12420  gcdmultipled  12429  bezoutlemb  12436  pcmpt  12781  4sqlem11  12839  mulgnn0dir  13603  limcimolemlt  15251  dvcnp2cntop  15286  dvmptcmulcn  15308  dveflem  15313  dvef  15314  plymullem1  15335  sin0pilem1  15368  sin2kpi  15398  cos2kpi  15399  coshalfpim  15410  sinkpi  15434