Prove that $P \implies Q \vdash \neg Q \implies\lnot P$ I'm trying to prove $$P \implies Q \vdash \neg Q \implies\lnot P$$
with natural deduction but I'm kind of stuck. I tried going from the conclusion side, which lead me to this:
$$ \frac{\frac{[P] \quad
\bot}{[\neg Q] \qquad
\neg P \qquad(\neg E)}}{\qquad\neg Q\implies \neg P \qquad (\implies E)}
$$
which is where I'm kind of stuck
 A: Unfortunately, (1) I don't know of a good way of drawing proof trees in MathJax and (2) there is no universally agreed set of natural deduction rules. Here is a proof presented as a sequence of labelled steps using rules similar to those presented here.
$$\begin{align*}
1 \quad& P \Rightarrow Q & \quad & \mbox{ASM - left open} \\
2 \quad& \lnot Q && \mbox{ASM - discharged at step 7} \\
3 \quad& P && \mbox{ASM - discharged at step 6} \\
4 \quad& Q && \mbox{1, 3, $\Rightarrow$-E} \\
5 \quad& \bot && \mbox{2, 4, $\lnot$-E} \\
6 \quad& \lnot P && \mbox{3, 5, $\lnot$-I} \\
7 \quad& \lnot Q \Rightarrow \lnot P && \mbox{2,6, $\Rightarrow$-I}
\end{align*}$$
Giving us $1 \vdash 7$, i.e., $P \Rightarrow Q \vdash \lnot Q \Rightarrow \lnot P$.

Here is a proof tree for the above that Graham Kemp has kindly added:
$$\sf\dfrac{\dfrac{\dfrac{\qquad\dfrac{P\to Q\quad{[P]}^2}{Q}{\small{\to}\rm E}\quad\lower{1.5ex}{{[\lnot Q]}^1}}{\bot}{\small\lnot\rm E}}{\lnot P}{\small\lnot\rm I^2}}{\lnot Q\to\lnot P\qquad}{\small{\to}\rm I^1}$$
A: (Posted after previous answer was accepted 3 hours ago)
Same proof, but this may be a little more readable format (screenshot from my proof checker):

