Theorem addid1d 7782

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

Syntax hints:   → wi 4   = wceq 1299   ∈ wcel 1448  (class class class)co 5706  ℂcc 7498  0cc0 7500   + caddc 7503

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

This theorem is referenced by:  subsub2  7861  negsub  7881  ltaddneg  8053  ltaddpos  8081  addge01  8101  add20  8103  apreap  8215  nnge1  8601  nnnn0addcl  8859  un0addcl  8862  peano2z  8942  zaddcl  8946  uzaddcl  9231  xaddid1  9486  fzosubel3  9814  expadd  10176  faclbnd6  10331  omgadd  10389  reim0b  10475  rereb  10476  immul2  10493  resqrexlemcalc3  10628  resqrexlemnm  10630  max0addsup  10831  fsumsplit  11015  sumsplitdc  11040  bezoutlema  11480  trilpolemlt1  12818