Metamath Proof Explorer


Theorem 4t2e8

Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion 4t2e8 4 2 = 8

Proof

Step Hyp Ref Expression
1 4cn 4
2 1 times2i 4 2 = 4 + 4
3 4p4e8 4 + 4 = 8
4 2 3 eqtri 4 2 = 8