Prove $Q \rightarrow \neg(Q \rightarrow \neg P)$ I have an exercise about proving statements:

Suppose that P is true. Prove that Q → ¬(Q → ¬P ) is true

Givens:
$P$
$Q \rightarrow \neg P$
Goal:
$\neg Q$
which I simply prove by contrapositive in this way:
$Q \rightarrow \neg P$ is equivalent to $P \rightarrow \neg Q$, which is what we wanted to prove, right?
 A: I see that you are proving $Q → ¬(Q → ¬P )$ by contrapositive, given $P$ as a premise.
So you are trying to prove, along with the premise $P$, $\lnot\lnot (Q\rightarrow \lnot P) \rightarrow \lnot Q \iff (Q\rightarrow \lnot P) \rightarrow \lnot Q$
You're almost there. 
Assuming $P\rightarrow \lnot Q$ is certainly equivalent to assuming $ Q \rightarrow \lnot P$.
But we need something more to conclude, therefore $\lnot Q$.
Specifically, assuming $P\rightarrow \lnot Q$, 
to use along with the given premise $P$, 
by modus ponens, give us $\lnot Q, as desired.
A: In the system that I learnt:
Assume $P$
Assume $Q$
Assume $(Q \rightarrow \lnot P)$
Modus Ponens: $\lnot P$. 
Contradiction so we withdraw $(Q \rightarrow \lnot P)$
and conclude
$\lnot(Q \rightarrow \lnot P)$ 
So introduction of $\rightarrow$ rule: (withdraw $Q$ and)
$Q \rightarrow \lnot(Q \rightarrow \lnot P)$
A: Remember that $\lnot X$ is equivalent to $X \to \bot$. Using the convention that $A \to B \to C$ means $A \to (B \to C)$, and expanding the negations, you want to prove
$$
P \to Q \to (Q \to P \to \bot) \to \bot
$$
Also remember that
$A \to B \to C$ is equivalent to $(A \land B) \to C$; this is called "Currying". Using Currying twice, you want to prove
$$
(P \land Q) \to ((P \land Q) \to \bot) \to \bot
$$
Applying Currying one more time, you want to prove
$$
((P \land Q) \land ((P \land Q) \to \bot)) \to \bot
$$
This final formula is an instance of the logical axiom modus ponens: $(X \land (X \to Y)) \to Y$.
Note that this is a direct proof: no contradiction or contrapositive was used. 
A: $
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\\ #1 \quad & \quad \text{"#2"} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\Tag}[1]{\text{(#1)}}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
\newcommand{\then}{\to}
\newcommand{\iff}{\leftrightarrow}
$In another proof system than the previous answers: assume $\;Q\;$ is true, and simplify the consequent step by (baby) step:
$$\calc
\lnot(Q \then \lnot P)
\calcop\iff{use assumption $\;Q\;$}
\lnot(\true \then \lnot P)
\calcop\iff{simplify}
\lnot \false
\calcop\iff{simplify}
\true
\endcalc$$
Therefore $\;Q \then \lnot(Q \then \lnot P)\;$.
