Theorem 8p7e15

Description: 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	8p7e15	$$⊢8+7=15$$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4		df-7	$$⊢7=6+1$$
5		df-5	$$⊢5=4+1$$
6		8p6e14	$$⊢8+6=14$$
7	1 2 3 4 5 6	6p5lem	$$⊢8+7=15$$