Metamath Proof Explorer

Theorem 7t2e14

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

Ref Expression
Assertion 7t2e14 
|- ( 7 x. 2 ) = ; 1 4

Proof

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