Theorem addid1d 7257

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

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433  (class class class)co 5532  ℂcc 6979  0cc0 6981   + caddc 6984

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

This theorem is referenced by:  subsub2  7336  negsub  7356  ltaddneg  7528  ltaddpos  7556  addge01  7576  add20  7578  apreap  7687  nnge1  8062  nnnn0addcl  8318  un0addcl  8321  peano2z  8387  zaddcl  8391  uzaddcl  8674  fzosubel3  9205  expadd  9518  faclbnd6  9671  reim0b  9749  rereb  9750  immul2  9767  resqrexlemcalc3  9902  resqrexlemnm  9904  max0addsup  10105  bezoutlema  10388