Theorem addlidd 8483

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   0cc0 8185   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-addcom 8285  ax-i2m1 8290  ax-0id 8293

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  negeu  8524  ltadd2  8754  subge0  8810  sublt0d  8906  un0addcl  9607  lincmb01cmp  10421  modsumfzodifsn  10853  bcm1n  11228  ccatlid  11395  swrdfv0  11447  swrdpfx  11500  pfxpfx  11501  cats1un  11514  swrdccatin2  11522  cats1fvnd  11558  rennim  11789  max0addsup  12007  fsumsplit  12198  sumsplitdc  12223  fisum0diag2  12238  isumsplit  12282  arisum2  12290  efaddlem  12465  eftlub  12481  ef4p  12485  moddvds  12590  gcdaddm  12785  gcdmultipled  12794  bezoutlemb  12801  pcmpt  13150  4sqlem11  13208  mulgnn0dir  14013  limcimolemlt  15907  dvcnp2cntop  15942  dvmptcmulcn  15964  dveflem  15969  dvef  15970  plymullem1  15991  sin0pilem1  16025  sin2kpi  16055  cos2kpi  16056  coshalfpim  16067  sinkpi  16091  logfac  16143  chtublem  16312