Theorem addid2d 8120

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
addid2d	|- ( ph -> ( 0 + A ) = A )

Proof of Theorem addid2d

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addlid 8109	. 2 |- ( A e. CC -> ( 0 + A ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1363   e. wcel 2158  (class class class)co 5888   CCcc 7822   0cc0 7824   + caddc 7827

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1cn 7917  ax-icn 7919  ax-addcl 7920  ax-mulcl 7922  ax-addcom 7924  ax-i2m1 7929  ax-0id 7932

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  negeu  8161  ltadd2  8389  subge0  8445  sublt0d  8540  un0addcl  9222  lincmb01cmp  10016  modsumfzodifsn  10409  rennim  11024  max0addsup  11241  fsumsplit  11428  sumsplitdc  11453  fisum0diag2  11468  isumsplit  11512  arisum2  11520  efaddlem  11695  eftlub  11711  ef4p  11715  moddvds  11819  gcdaddm  11998  gcdmultipled  12007  bezoutlemb  12014  pcmpt  12354  mulgnn0dir  13044  limcimolemlt  14404  dvcnp2cntop  14434  dvmptcmulcn  14454  dveflem  14458  dvef  14459  sin0pilem1  14473  sin2kpi  14503  cos2kpi  14504  coshalfpim  14515  sinkpi  14539