Deduction of contraposition propositional logic

Question

I have to find a deduction whose conclusion is the law of contraposition: $(\varphi \rightarrow \psi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$.

In particular it is suggested we use the following axioms:

1. $\varphi \rightarrow (\psi \rightarrow \varphi)$
2. $(\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \neg \psi) \rightarrow \neg \varphi)$

This is as far as I've gotten, but in the end the result is a tautology and not my intended formula:

1. $\varphi \rightarrow \psi \vdash \neg \psi \rightarrow \neg \varphi$ [Deduction theorem]
2. $(\neg \psi \rightarrow \neg \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\neg \psi \rightarrow \neg \varphi))$ [Iteration of 1.]
3. $\varphi \rightarrow \psi$ [Assumption]
4. $(\neg \psi \rightarrow \neg \varphi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$ [Modus ponens of 2 and 3]

How can I get from $(\neg \psi \rightarrow \neg \varphi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$ to $(\neg \psi \rightarrow \neg \varphi)$?

Thank you very much in advance!

Answer 1

Assume the antecedent of (($\phi$$\rightarrow$$\psi$)$\rightarrow$($\lnot$$\psi$$\rightarrow$$\lnot$$\phi$)).

Then apply 2. and detach something, which I'll call "something".

Now assume the second antecedent of the above '$\lnot$$\psi$'. Then apply axiom 1 and detach something that matches the antecedent of "something".

And I hope you can then find the last step.

Edit:

In Polish notation we have the following as axioms:

1. CaCba
2. CCabCCaNbNa

Here's a diagram:

    CCabCCaNbNa    Cab   C a  C b a
      \           /        |    | |
       \         /         --   | --
        \       / Nb     C Nb C a Nb
         \     /   \    /
          CCaNbNa  CaNb
              \    /
                Na