Theorem addridd 8483

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184  0cc0 8186   + caddc 8189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 8294

This theorem is used by:  subsub2  8562  negsub  8582  ltaddneg  8760  ltaddpos  8788  addge01  8808  add20  8810  apreap  8924  nnge1  9337  nnnn0addcl  9605  un0addcl  9608  peano2z  9692  zaddcl  9696  uzaddcl  10003  xaddid1  10282  fzosubel3  10632  expadd  11040  faclbnd6  11205  omgadd  11265  ccatrid  11398  pfxmpt  11475  pfxfv  11479  pfxswrd  11501  pfxccatin12lem1  11523  pfxccatin12lem2  11526  swrdccat3blem  11534  reim0b  11650  rereb  11651  immul2  11668  resqrexlemcalc3  11805  resqrexlemnm  11807  max0addsup  12009  fsumsplit  12200  sumsplitdc  12225  bitsinv1lem  12754  bezoutlema  12802  pcadd  13149  pcadd2  13150  pcmpt  13152  mulgnn0dir  14015  cosmpi  16055  sinppi  16056  sinhalfpip  16059  zprmlogbaplem2  16228  vtxdumgrfival  16756  p1evtxdeqfi  16770  eupth2lem3lem6fi  16929  trilpolemlt1  17309