Theorem 6t4e24

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

	Ref	Expression
Assertion	6t4e24	$$⊢6\cdot 4=24$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		3nn0	$$⊢3\in {\mathbb{N}}_0$$
3		df-4	$$⊢4=3+1$$
4		6t3e18	$$⊢6\cdot 3=18$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		eqid	$$⊢18=18$$
8		1p1e2	$$⊢1+1=2$$
9		4nn0	$$⊢4\in {\mathbb{N}}_0$$
10		8p6e14	$$⊢8+6=14$$
11	5 6 1 7 8 9 10	decaddci	$$⊢18+6=24$$
12	1 2 3 4 11	4t3lem	$$⊢6\cdot 4=24$$