Metamath Proof Explorer


Theorem addid1i

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 addid1i
|- ( A + 0 ) = A

Proof

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