Theorem 5t3e15

Description: 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Assertion	5t3e15	$$⊢5\cdot 3=15$$

Proof

Step	Hyp	Ref	Expression
1		5nn0	$$⊢5\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		df-3	$$⊢3=2+1$$
4		5t2e10	$$⊢5\cdot 2=10$$
5		dec10p	$$⊢10+5=15$$
6	1 2 3 4 5	4t3lem	$$⊢5\cdot 3=15$$