using modus ponens to deduce $(\neg A \rightarrow \neg B) \rightarrow ((\neg A \rightarrow B) \rightarrow A)$ Given The following 3 axioms: 


*

*$B \rightarrow (A \rightarrow B)$

*$(B \rightarrow (A \rightarrow C)) \rightarrow ((B \rightarrow A) \rightarrow (B \rightarrow C))$ 

*$(\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$ 
Can any one give any hint on how to prove  $(\neg A \rightarrow \neg B) \rightarrow ((\neg A \rightarrow B) \rightarrow A)$ using only modus ponens? 
 A: I assume you can use the Deduction Theorem, because without that, this would be a really nasty proof.
OK, first let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:
\begin{array}{lll}
1. & \phi \to \psi & Premise\\
2. & \psi \to \chi & Premise\\
3. & \phi & Premise\\
4. & \psi & MP \ 1,3\\
5. & \chi & MP \ 2,4\\
\end{array}
By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$
OK, now let's use HS to prove Duns Scotus Law: $\vdash \neg \phi \to (\phi \to \psi)$
\begin{array}{lll}
1. & \neg \phi \to (\neg \psi \to \neg \phi) &  Axiom \ 1\\
2. & (\neg \psi \to \neg \phi) \to (\phi \to \psi) & Axiom \ 3\\
3. & \neg \phi \to (\phi \to \psi) & HS \ 1,2
\end{array}
Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$
\begin{array}{lll}
1. & \neg \phi \to \phi & Premise\\
2. & \neg \phi \to (\phi \to \neg (\neg \phi \to \phi)) & Duns \ Scotus \ Law\\
3. & (\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))) &  Axiom \ 2\\
4. & (\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)) &  MP \ 2,3\\
5. & \neg \phi \to \neg (\neg \phi \to \phi) & MP \ 1,4\\
6. & (\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi) & Axiom \ 3\\
7. & (\neg \phi \to \phi) \to \phi &  MP \ 5,6\\
8. & \phi & MP \ 1,7\\
\end{array}
By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)
OK, now we can show $\neg \phi \to \psi, \neg \phi \to \neg \psi \vdash \phi$:
\begin{array}{lll}
1 & \neg \phi \to \psi & Premise\\
2 &  \neg \phi \to \neg \psi & Premise\\
3 & (\neg \phi \to \neg \psi) \to (\psi \to \phi) & Axiom \ 3\\
4 & \psi \to \phi & MP \ 2,3\\
5 & \neg \phi \to \phi & HS \ 1,4\\
6 & (\neg \phi \to \phi) \to \phi & Law \ of \ Clavius\\
7 & \phi & MP \ 5,6\\
\end{array}
Applying the Deduction Theorem twice, we have finally get the statement we want: $\vdash (\neg \phi \to \psi) \to ((\neg \phi \to \neg \psi) \to \phi)$
A: I assume the OP has at least the conjugation rule $A, B \therefore A \wedge B$. Alternatively, we can simply define an indirect proof to stop whenever $\neg A$ and $A$ occur in the proof.
\begin{array}{l|lr}
1 & B \rightarrow (A \rightarrow B) & \qquad\text{Assumption}
\\2 & (B \rightarrow (A \rightarrow C)) \rightarrow ((B \rightarrow A) \rightarrow (B \rightarrow C)) & \qquad\text{Assumption}
\\3 & (\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A) & \qquad\text{Assumption}
\\[0pt]\hline
\\[-5pt]4 & \neg A \rightarrow \neg B & \qquad\text{conditional proof}
\\5 & B \rightarrow A & \qquad\text{3,4 MP}
\\6 & \neg A \rightarrow  B & \qquad\text{conditional proof}
\\7 & \neg A & \qquad\text{Indirect proof}
\\8 & \neg B & \qquad\text{4,7 MP}
\\9 &  B & \qquad\text{6,7 MP}
\\10 & \neg B \wedge B & \qquad\text{8,9 Conj}
\\11 & A & \qquad\text{7-10 IP}
\\12 & (\neg A \rightarrow  B) \rightarrow A & \qquad\text{6-11 CP}
\\13 & (\neg A \rightarrow \neg B) \rightarrow ((\neg A \rightarrow B) \rightarrow A) & \qquad\text{4-12 CP}
\end{array} 
