Theorem addid2d 7936

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   0cc0 7644   + caddc 7647

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-addcom 7744  ax-i2m1 7749  ax-0id 7752

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  negeu  7977  ltadd2  8205  subge0  8261  sublt0d  8356  un0addcl  9034  lincmb01cmp  9816  modsumfzodifsn  10200  rennim  10806  max0addsup  11023  fsumsplit  11208  sumsplitdc  11233  fisum0diag2  11248  isumsplit  11292  arisum2  11300  efaddlem  11417  eftlub  11433  ef4p  11437  moddvds  11538  gcdaddm  11708  gcdmultipled  11717  bezoutlemb  11724  limcimolemlt  12841  dvcnp2cntop  12871  dvmptcmulcn  12891  dveflem  12895  dvef  12896  sin0pilem1  12910  sin2kpi  12940  cos2kpi  12941  coshalfpim  12952  sinkpi  12976