Theorem addlidd 8143

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160  (class class class)co 5900   CCcc 7844   0cc0 7846   + caddc 7849

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7939  ax-icn 7941  ax-addcl 7942  ax-mulcl 7944  ax-addcom 7946  ax-i2m1 7951  ax-0id 7954

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  negeu  8184  ltadd2  8412  subge0  8468  sublt0d  8563  un0addcl  9245  lincmb01cmp  10040  modsumfzodifsn  10434  rennim  11053  max0addsup  11270  fsumsplit  11457  sumsplitdc  11482  fisum0diag2  11497  isumsplit  11541  arisum2  11549  efaddlem  11724  eftlub  11740  ef4p  11744  moddvds  11848  gcdaddm  12027  gcdmultipled  12036  bezoutlemb  12043  pcmpt  12387  4sqlem11  12445  mulgnn0dir  13118  limcimolemlt  14636  dvcnp2cntop  14666  dvmptcmulcn  14686  dveflem  14690  dvef  14691  sin0pilem1  14705  sin2kpi  14735  cos2kpi  14736  coshalfpim  14747  sinkpi  14771