Metamath Proof Explorer

Theorem 6t2e12

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

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

Proof

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