Theorem addid1d 8038

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

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

Assertion

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

Proof of Theorem addid1d

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

Syntax hints:   → wi 4   = wceq 1342   ∈ wcel 2135  (class class class)co 5836  ℂcc 7742  0cc0 7744   + caddc 7747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7852

This theorem is referenced by:  subsub2  8117  negsub  8137  ltaddneg  8313  ltaddpos  8341  addge01  8361  add20  8363  apreap  8476  nnge1  8871  nnnn0addcl  9135  un0addcl  9138  peano2z  9218  zaddcl  9222  uzaddcl  9515  xaddid1  9789  fzosubel3  10121  expadd  10487  faclbnd6  10646  omgadd  10704  reim0b  10790  rereb  10791  immul2  10808  resqrexlemcalc3  10944  resqrexlemnm  10946  max0addsup  11147  fsumsplit  11334  sumsplitdc  11359  bezoutlema  11917  pcadd  12248  pcmpt  12250  cosmpi  13278  sinppi  13279  sinhalfpip  13282  trilpolemlt1  13754