Metamath Proof Explorer

Theorem 8t2e16

Description: 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 8t2e16 
|- ( 8 x. 2 ) = ; 1 6

Proof

Step Hyp Ref Expression
1 8cn 
 |-  8 e. CC
2 1 times2i 
 |-  ( 8 x. 2 ) = ( 8 + 8 )
3 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
4 2 3 eqtri 
 |-  ( 8 x. 2 ) = ; 1 6