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

Metamath Proof Explorer

Theorem 4t3e12

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

		Ref	Expression
	Assertion	4t3e12	$⊢ 4 \cdot 3 = 12$

Step	Hyp	Ref	Expression
1		4nn0	$⊢ 4 \in ℕ_{0}$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3		df-3	$⊢ 3 = 2 + 1$
4		4t2e8	$⊢ 4 \cdot 2 = 8$
5		8p4e12	$⊢ 8 + 4 = 12$
6	1 2 3 4 5	4t3lem	$⊢ 4 \cdot 3 = 12$