Theorem addid2d 8109

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   0cc0 7813   + caddc 7816

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-addcom 7913  ax-i2m1 7918  ax-0id 7921

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  negeu  8150  ltadd2  8378  subge0  8434  sublt0d  8529  un0addcl  9211  lincmb01cmp  10005  modsumfzodifsn  10398  rennim  11013  max0addsup  11230  fsumsplit  11417  sumsplitdc  11442  fisum0diag2  11457  isumsplit  11501  arisum2  11509  efaddlem  11684  eftlub  11700  ef4p  11704  moddvds  11808  gcdaddm  11987  gcdmultipled  11996  bezoutlemb  12003  pcmpt  12343  mulgnn0dir  13018  limcimolemlt  14218  dvcnp2cntop  14248  dvmptcmulcn  14268  dveflem  14272  dvef  14273  sin0pilem1  14287  sin2kpi  14317  cos2kpi  14318  coshalfpim  14329  sinkpi  14353