Theorem addridi 8470

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 8466	. 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 8178  0cc0 8180   + caddc 8183

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

This theorem is used by:  1p0e1  9423  9p1e10  9784  num0u  9792  numnncl2  9809  decrmanc  9843  decaddi  9846  decaddci  9847  decmul1  9850  decmulnc  9853  fsumrelem  12257  demoivreALT  12560  decsplit0  13230  37prm  13258  43prm  13259  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  ballotfilemth  13333  sinhalfpilem  15984  efipi  15994  log2ublem3  16189  log2ublog2  16190