Metamath Proof Explorer


Theorem 9p8e17

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

Ref Expression
Assertion 9p8e17 9+8=17

Proof

Step Hyp Ref Expression
1 9nn0 90
2 7nn0 70
3 6nn0 60
4 df-8 8=7+1
5 df-7 7=6+1
6 9p7e16 9+7=16
7 1 2 3 4 5 6 6p5lem 9+8=17