Metamath Proof Explorer

Theorem 3exp3

Description: Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 3exp3 
|- ( 3 ^ 3 ) = ; 2 7

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 2nn0 
 |-  2 e. NN0
3 2p1e3 
 |-  ( 2 + 1 ) = 3
4 sq3 
 |-  ( 3 ^ 2 ) = 9
5 4 oveq1i 
 |-  ( ( 3 ^ 2 ) x. 3 ) = ( 9 x. 3 )
6 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
7 5 6 eqtri 
 |-  ( ( 3 ^ 2 ) x. 3 ) = ; 2 7
8 1 2 3 7 numexpp1 
 |-  ( 3 ^ 3 ) = ; 2 7