Theorem addridd 8228

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

Hypothesis

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

Assertion

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

Proof of Theorem addridd

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930  0cc0 7932   + caddc 7935

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

This theorem is referenced by:  subsub2  8307  negsub  8327  ltaddneg  8504  ltaddpos  8532  addge01  8552  add20  8554  apreap  8667  nnge1  9066  nnnn0addcl  9332  un0addcl  9335  peano2z  9415  zaddcl  9419  uzaddcl  9714  xaddid1  9991  fzosubel3  10332  expadd  10733  faclbnd6  10896  omgadd  10954  ccatrid  11071  pfxmpt  11139  pfxfv  11143  pfxswrd  11165  reim0b  11217  rereb  11218  immul2  11235  resqrexlemcalc3  11371  resqrexlemnm  11373  max0addsup  11574  fsumsplit  11762  sumsplitdc  11787  bitsinv1lem  12316  bezoutlema  12364  pcadd  12707  pcadd2  12708  pcmpt  12710  mulgnn0dir  13532  cosmpi  15332  sinppi  15333  sinhalfpip  15336  trilpolemlt1  16054