Metamath Proof Explorer

Theorem addridi

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

Ref Expression
Hypothesis mul.1 
|- A e. CC
Assertion addridi 
|- ( A + 0 ) = A

Proof

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