Theorem addlidd 8329

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   0cc0 8032   + caddc 8035

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-addcom 8132  ax-i2m1 8137  ax-0id 8140

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

This theorem is referenced by:  negeu  8370  ltadd2  8599  subge0  8655  sublt0d  8750  un0addcl  9435  lincmb01cmp  10238  modsumfzodifsn  10659  ccatlid  11187  swrdfv0  11239  swrdpfx  11292  pfxpfx  11293  cats1un  11306  swrdccatin2  11314  cats1fvnd  11350  rennim  11567  max0addsup  11784  fsumsplit  11973  sumsplitdc  11998  fisum0diag2  12013  isumsplit  12057  arisum2  12065  efaddlem  12240  eftlub  12256  ef4p  12260  moddvds  12365  gcdaddm  12560  gcdmultipled  12569  bezoutlemb  12576  pcmpt  12921  4sqlem11  12979  mulgnn0dir  13744  limcimolemlt  15394  dvcnp2cntop  15429  dvmptcmulcn  15451  dveflem  15456  dvef  15457  plymullem1  15478  sin0pilem1  15511  sin2kpi  15541  cos2kpi  15542  coshalfpim  15553  sinkpi  15577