This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 8t7e56

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

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

Step	Hyp	Ref	Expression
1		8nn0	$⊢ 8 \in ℕ_{0}$
2		6nn0	$⊢ 6 \in ℕ_{0}$
3		df-7	$⊢ 7 = 6 + 1$
4		8t6e48	$⊢ 8 \cdot 6 = 48$
5		4nn0	$⊢ 4 \in ℕ_{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$