Metamath Proof Explorer


Theorem times2i

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

Ref Expression
Hypothesis 2timesi.1 โŠข ๐ด โˆˆ โ„‚
Assertion times2i ( ๐ด ยท 2 ) = ( ๐ด + ๐ด )

Proof

Step Hyp Ref Expression
1 2timesi.1 โŠข ๐ด โˆˆ โ„‚
2 times2 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยท 2 ) = ( ๐ด + ๐ด ) )
3 1 2 ax-mp โŠข ( ๐ด ยท 2 ) = ( ๐ด + ๐ด )