Theorem addid2d 7912

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   0cc0 7620   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-addcom 7720  ax-i2m1 7725  ax-0id 7728

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  negeu  7953  ltadd2  8181  subge0  8237  sublt0d  8332  un0addcl  9010  lincmb01cmp  9786  modsumfzodifsn  10169  rennim  10774  max0addsup  10991  fsumsplit  11176  sumsplitdc  11201  fisum0diag2  11216  isumsplit  11260  arisum2  11268  efaddlem  11380  eftlub  11396  ef4p  11400  moddvds  11502  gcdaddm  11672  gcdmultipled  11681  bezoutlemb  11688  limcimolemlt  12802  dvcnp2cntop  12832  dvmptcmulcn  12852  dveflem  12855  dvef  12856  sin0pilem1  12862  sin2kpi  12892  cos2kpi  12893  coshalfpim  12904  sinkpi  12928