Theorem 8p8e16

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

	Ref	Expression
Assertion	8p8e16	$$⊢8+8=16$$

Proof

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