Derive: $(B\to A)\to(\neg A\to\neg B)$ I've been trying to find a solution to this problem for about two hours. Can't make any more progress as I find it hard to come up with new theorems.
Problem
$$(B \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B) $$
I need to prove this using the three logical axioms and/or modus ponens. I know how to use all of these, but I'm having difficulty laying out the correct order of and/or correct intermediary steps.
UPDATE
These are the three axioms
1st) $$A \rightarrow (B \rightarrow A) $$
2nd) $$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) $$
3rd) $$((\lnot B) \rightarrow (\lnot A)) \rightarrow (A \rightarrow B) $$
 A: Translating $A \to B$ to $\lnot A \lor B$ is, in my opinion, cheating. It's possible to do this directly from the axioms. In fact, you don't even need the third one. Let's call your first axiom K and your second axiom S. We can prove this without the third axiom. Your question amounts to asking the following question in combinatory logic: Can we find an expression in terms of K and S alone for the following lambda expression?
$$\lambda x . \, \lambda y . \, \lambda z . \, y (x z)$$
The answer, by general theory, is yes. Explicitly, 
$$S(K(S(S(K S)K)))K x y z = y (x z)$$
Hence our proof takes the following form. For the sake of brevity, we write
$$A = p \to q$$
$$B = \lnot q \to \lnot p$$
and more generally we write $[n]$ for the $n$-th expression in the list below.


*

*(Axiom S) $(A \to [11]) \to ([14] \to [15])$

*(Axiom K) $[11] \to (A \to [11])$

*(Axiom S) $[10] \to [11]$

*(Axiom S) $(\lnot q \to [6]) \to ([9] \to [10])$

*(Axiom K) $[6] \to (\lnot q \to [6])$

*(Axiom S) $(p \to (q \to \bot)) \to ((p \to q) \to (p \to \bot))$

*(MP 5, 6) $\lnot q \to [6]$

*(MP 4, 7) $[9] \to [10]$

*(Axiom K) $\lnot q \to (p \to \lnot q)$

*(MP 8, 9) $\lnot q \to (A \to \lnot p)$

*(MP 3, 10) $(\lnot q \to A) \to B$

*(MP 2, 11) $A \to [11]$

*(MP 1, 12) $[14] \to [15]$

*(Axiom K) $A \to (\lnot q \to A)$

*(MP 13, 14) $A \to B$


In full gory detail:


*

*(Axiom S) $(A \to ((\lnot q \to A) \to B)) \to ((A \to (\lnot q \to A)) \to (A \to B))$

*(Axiom K) $((\lnot q \to A) \to B) \to (A \to ((\lnot q \to A) \to B))$

*(Axiom S) $(\lnot q \to (A \to \lnot p)) \to ((\lnot q \to A) \to B)$

*(Axiom S) $(\lnot q \to ((p \to \lnot q) \to (A \to \lnot p))) \to ((\lnot q \to (p \to \lnot q)) \to (\lnot q \to (A \to \lnot p)))$

*(Axiom K) $((p \to \lnot q) \to (A \to \lnot p)) \to (\lnot q \to ((p \to \lnot q) \to (A \to \lnot p)))$

*(Axiom S) $(p \to \lnot q) \to (A \to \lnot p)$

*(MP 5, 6) $\lnot q \to ((p \to \lnot q) \to (A \to \lnot p))$

*(MP 4, 7) $(\lnot q \to (p \to \lnot q)) \to (\lnot q \to (A \to \lnot p))$

*(Axiom K) $\lnot q \to (p \to \lnot q)$

*(MP 8, 9) $\lnot q \to (A \to \lnot p)$

*(MP 3, 10) $(\lnot q \to A) \to B$

*(MP 2, 11) $A \to ((\lnot q \to A) \to B)$

*(MP 1, 12) $(A \to (\lnot q \to A)) \to (A \to B)$

*(Axiom K) $A \to (\lnot q \to A)$

*(MP 13, 14) $A \to B$


Exercise for enthusiasts. Find a shorter proof, or show that this proof is minimal.
A: the definition of $X\to Y$ is: $Y\lor  \neg X$
if you translate the $\neg A\to\neg B$
to its definition you will get the same as for $B \to A$.
