Theorem addid2d 7632

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

Syntax hints:   -> wi 4   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7348   0cc0 7350   + caddc 7353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7438  ax-icn 7440  ax-addcl 7441  ax-mulcl 7443  ax-addcom 7445  ax-i2m1 7450  ax-0id 7453

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  negeu  7673  ltadd2  7897  subge0  7953  sublt0d  8047  un0addcl  8706  lincmb01cmp  9420  modsumfzodifsn  9803  rennim  10435  max0addsup  10652  fsumsplit  10801  sumsplitdc  10826  fisum0diag2  10841  isumsplit  10885  arisum2  10893  efaddlem  10964  eftlub  10980  ef4p  10984  moddvds  11083  gcdaddm  11253  bezoutlemb  11267