Metamath Proof Explorer

Theorem 9t2e18

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

Ref Expression
Assertion 9t2e18 
|- ( 9 x. 2 ) = ; 1 8

Proof

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