Metamath Proof Explorer


Theorem times2i

Description: A number times 2. (Contributed by NM, 11-May-2004)

Ref Expression
Hypothesis 2timesi.1
|- A e. CC
Assertion times2i
|- ( A x. 2 ) = ( A + A )

Proof

Step Hyp Ref Expression
1 2timesi.1
 |-  A e. CC
2 times2
 |-  ( A e. CC -> ( A x. 2 ) = ( A + A ) )
3 1 2 ax-mp
 |-  ( A x. 2 ) = ( A + A )