Metamath Proof Explorer


Theorem 2exp4

Description: Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 2exp4 2 4 = 16

Proof

Step Hyp Ref Expression
1 2nn0 2 0
2 2t2e4 2 2 = 4
3 sq2 2 2 = 4
4 4t4e16 4 4 = 16
5 1 1 2 3 4 numexp2x 2 4 = 16