Theorem addlidd 8284

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 5994   CCcc 7985   0cc0 7987   + caddc 7990

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8080  ax-icn 8082  ax-addcl 8083  ax-mulcl 8085  ax-addcom 8087  ax-i2m1 8092  ax-0id 8095

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  negeu  8325  ltadd2  8554  subge0  8610  sublt0d  8705  un0addcl  9390  lincmb01cmp  10187  modsumfzodifsn  10605  ccatlid  11127  swrdfv0  11172  swrdpfx  11225  pfxpfx  11226  cats1un  11239  swrdccatin2  11247  cats1fvnd  11283  rennim  11499  max0addsup  11716  fsumsplit  11904  sumsplitdc  11929  fisum0diag2  11944  isumsplit  11988  arisum2  11996  efaddlem  12171  eftlub  12187  ef4p  12191  moddvds  12296  gcdaddm  12491  gcdmultipled  12500  bezoutlemb  12507  pcmpt  12852  4sqlem11  12910  mulgnn0dir  13675  limcimolemlt  15323  dvcnp2cntop  15358  dvmptcmulcn  15380  dveflem  15385  dvef  15386  plymullem1  15407  sin0pilem1  15440  sin2kpi  15470  cos2kpi  15471  coshalfpim  15482  sinkpi  15506