Theorem addlidd 8372

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 8361	. 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 2202  (class class class)co 6028   CCcc 8073   0cc0 8075   + caddc 8078

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 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-addcom 8175  ax-i2m1 8180  ax-0id 8183

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

This theorem is referenced by:  negeu  8413  ltadd2  8642  subge0  8698  sublt0d  8793  un0addcl  9478  lincmb01cmp  10281  modsumfzodifsn  10702  ccatlid  11230  swrdfv0  11282  swrdpfx  11335  pfxpfx  11336  cats1un  11349  swrdccatin2  11357  cats1fvnd  11393  rennim  11623  max0addsup  11840  fsumsplit  12029  sumsplitdc  12054  fisum0diag2  12069  isumsplit  12113  arisum2  12121  efaddlem  12296  eftlub  12312  ef4p  12316  moddvds  12421  gcdaddm  12616  gcdmultipled  12625  bezoutlemb  12632  pcmpt  12977  4sqlem11  13035  mulgnn0dir  13800  limcimolemlt  15455  dvcnp2cntop  15490  dvmptcmulcn  15512  dveflem  15517  dvef  15518  plymullem1  15539  sin0pilem1  15572  sin2kpi  15602  cos2kpi  15603  coshalfpim  15614  sinkpi  15638