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  10422  modsumfzodifsn  10854  bcm1n  11229  ccatlid  11396  swrdfv0  11448  swrdpfx  11501  pfxpfx  11502  cats1un  11515  swrdccatin2  11523  cats1fvnd  11559  rennim  11790  max0addsup  12008  fsumsplit  12199  sumsplitdc  12224  fisum0diag2  12239  isumsplit  12283  arisum2  12291  efaddlem  12466  eftlub  12482  ef4p  12486  moddvds  12591  gcdaddm  12786  gcdmultipled  12795  bezoutlemb  12802  pcmpt  13151  4sqlem11  13209  mulgnn0dir  14014  limcimolemlt  15890  dvcnp2cntop  15925  dvmptcmulcn  15947  dveflem  15952  dvef  15953  plymullem1  15974  sin0pilem1  16008  sin2kpi  16038  cos2kpi  16039  coshalfpim  16050  sinkpi  16074  logfac  16126  chtublem  16295