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	|- A e. CC

Assertion

Ref	Expression
addridi	|- ( A + 0 ) = A

Proof of Theorem addridi

Step	Hyp	Ref	Expression
1		mul.1	. 2 |- A e. CC
2		addrid 8464	. 2 |- ( A e. CC -> ( A + 0 ) = A )
3	1, 2	ax-mp 5	1 |- ( A + 0 ) = A

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

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

This theorem is used by:  1p0e1  9421  9p1e10  9781  num0u  9789  numnncl2  9801  decrmanc  9835  decaddi  9838  decaddci  9839  decmul1  9842  decmulnc  9845  fsumrelem  12240  demoivreALT  12543  decsplit0  13208  ballotfilemth  13283  sinhalfpilem  15895  efipi  15905  log2ublem3  16091  log2ublog2  16092