Theorem addridi 8468

Description: 0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addridi	⊢ (𝐴 + 0) = 𝐴

Proof of Theorem addridi

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		addrid 8464	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 + 0) = 𝐴

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  0cc0 8179   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-0id 8287

This theorem is used by:  1p0e1  9420  9p1e10  9779  num0u  9787  numnncl2  9799  decrmanc  9833  decaddi  9836  decaddci  9837  decmul1  9840  decmulnc  9843  fsumrelem  12238  demoivreALT  12541  decsplit0  13206  ballotfilemth  13281  sinhalfpilem  15893  efipi  15903  log2ublem3  16089  log2ublog2  16090