Theorem addridd 8263

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   + caddc 7970

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

This theorem is referenced by:  subsub2  8342  negsub  8362  ltaddneg  8539  ltaddpos  8567  addge01  8587  add20  8589  apreap  8702  nnge1  9101  nnnn0addcl  9367  un0addcl  9370  peano2z  9450  zaddcl  9454  uzaddcl  9749  xaddid1  10026  fzosubel3  10369  expadd  10770  faclbnd6  10933  omgadd  10991  ccatrid  11108  pfxmpt  11178  pfxfv  11182  pfxswrd  11204  pfxccatin12lem1  11226  pfxccatin12lem2  11229  swrdccat3blem  11237  reim0b  11339  rereb  11340  immul2  11357  resqrexlemcalc3  11493  resqrexlemnm  11495  max0addsup  11696  fsumsplit  11884  sumsplitdc  11909  bitsinv1lem  12438  bezoutlema  12486  pcadd  12829  pcadd2  12830  pcmpt  12832  mulgnn0dir  13655  cosmpi  15455  sinppi  15456  sinhalfpip  15459  trilpolemlt1  16320