Theorem 8t7e56

Description: 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	8t7e56	$$⊢8\cdot 7=56$$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		df-7	$$⊢7=6+1$$
4		8t6e48	$$⊢8\cdot 6=48$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6		eqid	$$⊢48=48$$
7		4p1e5	$$⊢4+1=5$$
8		8p8e16	$$⊢8+8=16$$
9	5 1 1 6 7 2 8	decaddci	$$⊢48+8=56$$
10	1 2 3 4 9	4t3lem	$$⊢8\cdot 7=56$$