Theorem addid1d 7904

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5767  ℂcc 7611  0cc0 7613   + caddc 7616

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

This theorem is referenced by:  subsub2  7983  negsub  8003  ltaddneg  8179  ltaddpos  8207  addge01  8227  add20  8229  apreap  8342  nnge1  8736  nnnn0addcl  9000  un0addcl  9003  peano2z  9083  zaddcl  9087  uzaddcl  9374  xaddid1  9638  fzosubel3  9966  expadd  10328  faclbnd6  10483  omgadd  10541  reim0b  10627  rereb  10628  immul2  10645  resqrexlemcalc3  10781  resqrexlemnm  10783  max0addsup  10984  fsumsplit  11169  sumsplitdc  11194  bezoutlema  11676  cosmpi  12886  sinppi  12887  sinhalfpip  12890  trilpolemlt1  13223