Theorem addridi 8476

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 8472	. 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 6088   CCcc 8184   0cc0 8186   + caddc 8189

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

This theorem is used by:  1p0e1  9430  9p1e10  9790  num0u  9798  numnncl2  9815  decrmanc  9849  decaddi  9852  decaddci  9853  decmul1  9856  decmulnc  9859  fsumrelem  12263  demoivreALT  12566  decsplit0  13236  37prm  13264  43prm  13265  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  ballotfilemth  13339  sinhalfpilem  16051  efipi  16061  log2ublem3  16256  log2ublog2  16257