Theorem addridd 8418

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  0cc0 8123   + caddc 8126

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

This theorem is referenced by:  subsub2  8497  negsub  8517  ltaddneg  8694  ltaddpos  8722  addge01  8742  add20  8744  apreap  8857  nnge1  9256  nnnn0addcl  9522  un0addcl  9525  peano2z  9609  zaddcl  9613  uzaddcl  9914  xaddid1  10191  fzosubel3  10537  expadd  10939  faclbnd6  11102  omgadd  11161  ccatrid  11288  pfxmpt  11365  pfxfv  11369  pfxswrd  11391  pfxccatin12lem1  11413  pfxccatin12lem2  11416  swrdccat3blem  11424  reim0b  11540  rereb  11541  immul2  11558  resqrexlemcalc3  11694  resqrexlemnm  11696  max0addsup  11897  fsumsplit  12086  sumsplitdc  12111  bitsinv1lem  12640  bezoutlema  12688  pcadd  13031  pcadd2  13032  pcmpt  13034  mulgnn0dir  13858  cosmpi  15668  sinppi  15669  sinhalfpip  15672  vtxdumgrfival  16280  p1evtxdeqfi  16294  eupth2lem3lem6fi  16453  trilpolemlt1  16812