Theorem addridd 8295

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6001  ℂcc 7997  0cc0 7999   + caddc 8002

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

This theorem is referenced by:  subsub2  8374  negsub  8394  ltaddneg  8571  ltaddpos  8599  addge01  8619  add20  8621  apreap  8734  nnge1  9133  nnnn0addcl  9399  un0addcl  9402  peano2z  9482  zaddcl  9486  uzaddcl  9781  xaddid1  10058  fzosubel3  10402  expadd  10803  faclbnd6  10966  omgadd  11024  ccatrid  11142  pfxmpt  11212  pfxfv  11216  pfxswrd  11238  pfxccatin12lem1  11260  pfxccatin12lem2  11263  swrdccat3blem  11271  reim0b  11373  rereb  11374  immul2  11391  resqrexlemcalc3  11527  resqrexlemnm  11529  max0addsup  11730  fsumsplit  11918  sumsplitdc  11943  bitsinv1lem  12472  bezoutlema  12520  pcadd  12863  pcadd2  12864  pcmpt  12866  mulgnn0dir  13689  cosmpi  15490  sinppi  15491  sinhalfpip  15494  trilpolemlt1  16409