Theorem addlidd 8422

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 8411	. 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 2203  (class class class)co 6049   CCcc 8124   0cc0 8126   + caddc 8129

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 2214  ax-1cn 8219  ax-icn 8221  ax-addcl 8222  ax-mulcl 8224  ax-addcom 8226  ax-i2m1 8231  ax-0id 8234

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  negeu  8463  ltadd2  8692  subge0  8748  sublt0d  8843  un0addcl  9528  lincmb01cmp  10335  modsumfzodifsn  10757  ccatlid  11290  swrdfv0  11342  swrdpfx  11395  pfxpfx  11396  cats1un  11409  swrdccatin2  11417  cats1fvnd  11453  rennim  11683  max0addsup  11900  fsumsplit  12089  sumsplitdc  12114  fisum0diag2  12129  isumsplit  12173  arisum2  12181  efaddlem  12356  eftlub  12372  ef4p  12376  moddvds  12481  gcdaddm  12676  gcdmultipled  12685  bezoutlemb  12692  pcmpt  13037  4sqlem11  13095  mulgnn0dir  13861  limcimolemlt  15521  dvcnp2cntop  15556  dvmptcmulcn  15578  dveflem  15583  dvef  15584  plymullem1  15605  sin0pilem1  15638  sin2kpi  15668  cos2kpi  15669  coshalfpim  15680  sinkpi  15704