Theorem addridd 8303

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005  0cc0 8007   + caddc 8010

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

This theorem is referenced by:  subsub2  8382  negsub  8402  ltaddneg  8579  ltaddpos  8607  addge01  8627  add20  8629  apreap  8742  nnge1  9141  nnnn0addcl  9407  un0addcl  9410  peano2z  9490  zaddcl  9494  uzaddcl  9789  xaddid1  10066  fzosubel3  10410  expadd  10811  faclbnd6  10974  omgadd  11032  ccatrid  11150  pfxmpt  11220  pfxfv  11224  pfxswrd  11246  pfxccatin12lem1  11268  pfxccatin12lem2  11271  swrdccat3blem  11279  reim0b  11381  rereb  11382  immul2  11399  resqrexlemcalc3  11535  resqrexlemnm  11537  max0addsup  11738  fsumsplit  11926  sumsplitdc  11951  bitsinv1lem  12480  bezoutlema  12528  pcadd  12871  pcadd2  12872  pcmpt  12874  mulgnn0dir  13697  cosmpi  15498  sinppi  15499  sinhalfpip  15502  trilpolemlt1  16439