Theorem addid2d 8069

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 8058	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772  0cc0 7774   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-addcom 7874  ax-i2m1 7879  ax-0id 7882

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  negeu  8110  ltadd2  8338  subge0  8394  sublt0d  8489  un0addcl  9168  lincmb01cmp  9960  modsumfzodifsn  10352  rennim  10966  max0addsup  11183  fsumsplit  11370  sumsplitdc  11395  fisum0diag2  11410  isumsplit  11454  arisum2  11462  efaddlem  11637  eftlub  11653  ef4p  11657  moddvds  11761  gcdaddm  11939  gcdmultipled  11948  bezoutlemb  11955  pcmpt  12295  limcimolemlt  13427  dvcnp2cntop  13457  dvmptcmulcn  13477  dveflem  13481  dvef  13482  sin0pilem1  13496  sin2kpi  13526  cos2kpi  13527  coshalfpim  13538  sinkpi  13562