Theorem addlidd 8439

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 8428	. 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  8480  ltadd2  8710  subge0  8766  sublt0d  8861  un0addcl  9546  lincmb01cmp  10355  modsumfzodifsn  10782  bcm1n  11156  ccatlid  11319  swrdfv0  11371  swrdpfx  11424  pfxpfx  11425  cats1un  11438  swrdccatin2  11446  cats1fvnd  11482  rennim  11712  max0addsup  11929  fsumsplit  12118  sumsplitdc  12143  fisum0diag2  12158  isumsplit  12202  arisum2  12210  efaddlem  12385  eftlub  12401  ef4p  12405  moddvds  12510  gcdaddm  12705  gcdmultipled  12714  bezoutlemb  12721  pcmpt  13066  4sqlem11  13124  mulgnn0dir  13953  limcimolemlt  15641  dvcnp2cntop  15676  dvmptcmulcn  15698  dveflem  15703  dvef  15704  plymullem1  15725  sin0pilem1  15758  sin2kpi  15788  cos2kpi  15789  coshalfpim  15800  sinkpi  15824