Theorem 6t3e18

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

	Ref	Expression
Assertion	6t3e18	$$⊢6\cdot 3=18$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		df-3	$$⊢3=2+1$$
4		6t2e12	$$⊢6\cdot 2=12$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		eqid	$$⊢12=12$$
7		6cn	$$⊢6\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9		6p2e8	$$⊢6+2=8$$
10	7 8 9	addcomli	$$⊢2+6=8$$
11	5 2 1 6 10	decaddi	$$⊢12+6=18$$
12	1 2 3 4 11	4t3lem	$$⊢6\cdot 3=18$$