Application of Modus Tollens rule in nested proof confusion

Question

From a book I'm reading for logic and computer science, the nested proof is as follows:

1. {$q \rightarrow r$ assumption

2. [$\neg q \rightarrow \neg p$ assumption

3. ( $p$ assumption

4. $\neg \neg p$ $\neg \neg i $ 3

5. $\neg \neg q$ $MT$ 2,4 (applying Modus Tollens)

6. $q$ $\neg \neg e$ 5

7. $r$ $\rightarrow e 1,6$ )

8. ... ]

9. ...

10. final proof}

note: sorry about the different brackets it was my attempt to show a nested proof.

my question is concerning how r in line number seven is derived. So, my first instinct tells me to apply the Modus Tollen rule to lines 2 and 3 and we can obtain $q$ that way, but I don't understand why do they apply the double negation rule to $p$ and didn't apply MT rule directly.

So, it would be

given the assumption of $\neg q \rightarrow \neg p$ given $p$

then we could derive $\vdash q$

Answer 1

Remember that modus tollens says that from $A\to B$ and $\neg B$ you can infer $\neg A$. So from $\neg q\to\neg p$ and $\neg \neg p$ you can infer $\neg\neg q$. That's why you need to use the rules to add (and then remove) the double negations even though those rules seem unnecessary to us in natural language.