Theorem addid2d 8081

Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addid2d	⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addid2 8070	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2146  (class class class)co 5865  ℂcc 7784  0cc0 7786   + caddc 7789

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157  ax-1cn 7879  ax-icn 7881  ax-addcl 7882  ax-mulcl 7884  ax-addcom 7886  ax-i2m1 7891  ax-0id 7894

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  negeu  8122  ltadd2  8350  subge0  8406  sublt0d  8501  un0addcl  9182  lincmb01cmp  9974  modsumfzodifsn  10366  rennim  10979  max0addsup  11196  fsumsplit  11383  sumsplitdc  11408  fisum0diag2  11423  isumsplit  11467  arisum2  11475  efaddlem  11650  eftlub  11666  ef4p  11670  moddvds  11774  gcdaddm  11952  gcdmultipled  11961  bezoutlemb  11968  pcmpt  12308  mulgnn0dir  12873  limcimolemlt  13704  dvcnp2cntop  13734  dvmptcmulcn  13754  dveflem  13758  dvef  13759  sin0pilem1  13773  sin2kpi  13803  cos2kpi  13804  coshalfpim  13815  sinkpi  13839