Theorem 6t4e24

Description: 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	6t4e24	|- ( 6 x. 4 ) = ; 2 4

Proof

Step	Hyp	Ref	Expression
1		6nn0	|- 6 e. NN0
2		3nn0	|- 3 e. NN0
3		df-4	|- 4 = ( 3 + 1 )
4		6t3e18	|- ( 6 x. 3 ) = ; 1 8
5		1nn0	|- 1 e. NN0
6		8nn0	|- 8 e. NN0
7		eqid	|- ; 1 8 = ; 1 8
8		1p1e2	|- ( 1 + 1 ) = 2
9		4nn0	|- 4 e. NN0
10		8p6e14	|- ( 8 + 6 ) = ; 1 4
11	5 6 1 7 8 9 10	decaddci	|- ( ; 1 8 + 6 ) = ; 2 4
12	1 2 3 4 11	4t3lem	|- ( 6 x. 4 ) = ; 2 4