Hilbert System with propositional logic $p \rightarrow q,\neg q \vdash \neg p$ This is my set of axiom


*

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

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

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


When applying it to prove
$$p \rightarrow q,\neg q \vdash \neg p$$
I get inside an exponential expansion which makes me feel it is not provable. So far I have been trying a several combinations in which start from A3 by substituting $A=\neg p$, $B=q$ and even with $B=\neg q$.
Is there any substitution that I am not seeing?
 A: This is a possible thought process. I don't have time to go through the details, but this seems to work.
Almost likely the formal proof of this theorem ends with an application of axiom 3 and modus ponens.
Axiom 3. with $A=\neg p$ and $B=q$ yields $$(\neg \neg p\to q)\to ((\neg \neg p\to \neg q)\to \neg p).$$
So it's enough to be able to deduce $\neg \neg p\to q$ and $\neg \neg p\to \neg q$.
Axiom 1 yields $\neg q\to(\neg \neg p\to \neg q)$, so $\neg \neg p\to \neg q$ is taken care of.
It remains to get $\neg \neg p\to q$. Since it is a conditional statement, it is likely a consequence of the second axiom.
The second axiom with $A=\neg \neg p, B=p$ and $C=q$ yields
$$(\neg \neg p\to (p\to q))\to ((\neg \neg p\to p)\to (\neg \neg p\to q)).$$
So now you want to use modus ponens on the above formula. Therefore it suffices to find proofs of $\neg \neg p\to (p\to q)$ and  $\neg \neg p\to p$. The first of these is easy. The other one is harder.
Proof of $\neg \neg p\to p$:
\begin{alignat*}{3}
1. \,&((\neg p\to \neg \neg p)\to p)\to (\neg \neg p\to ((\neg p \to \neg \neg p)\to p)) &&(\text A1)\\
 2. \,&(\neg p \to \neg p)\to ((\neg p\to \neg \neg p)\to p) &&(\text A3)\\
 3. \,&\neg p \to ((\neg p \to \neg p)\to \neg p) &&(\text{A} 1)\\
 4. \,&(\neg p\to ((\neg p \to \neg p)\to \neg p))\to ((\neg p \to (\neg p \to \neg p))\to (\neg p \to \neg p)) &&(\text{A} 2)\\
 5. \,&(\neg p \to (\neg p \to \neg p))\to (\neg p \to \neg p)  &&(\text{MP }3,4)\\
 6. \,&\neg p \to (\neg p\to \neg p) &&(\text{A}1)\\
 7. \,&\neg p \to \neg p &&(\text{MP }5,6)\\
 8. \,&(\neg p \to \neg \neg p)\to p &&(\text{MP }7,2)\\
 9. \,&\neg \neg p\to ((\neg p \to \neg \neg p)\to p) &&(\text{MP }8,1)\\
 10. \,&(\neg \neg p\to ((\neg p \to \neg \neg p)\to p))\to ((\neg \neg p\to (\neg p \to \neg \neg p))\to (\neg \neg p \to p)) &&(\text{A}2)\\
 11. \,&(\neg \neg p\to (\neg p \to \neg \neg p))\to (\neg \neg p \to p) &&(\text{MP 9,10})\\
 12. \,&\neg \neg p \to (\neg p \to \neg \neg p) &&(\text{A}1)\\
 13. \,&\neg \neg p \to p &&(\text{MP }12, 11)\\
\end{alignat*}
A: This answer is distinct from the last.
Axiom three tells us that if we have a negation implying a proposition, and also implying that proposition's negation, we can obtain the proposition.  So, since we want Np from {Cpq, Nq}, we might assume NNp.  We know that we should be able to get CNNpp in this system, since it's a tautology.  So, then we can get p, then q, and Nq.  Since we have NNp as our assumption, using the deduction theorem will yield CNNpq and CNNpNq.  With less work though, since we already have Nq as an assumption, we can get CNNpNq from CaCba and Nq.  Then having CCNabCCNaNba, CNNpq, and CNNpNq we can obtain Np after two detachments.
How do we get CNNpp?  Well, much in the same way that we can get to Np above.  We assume the negation of the consequent "p".  Since we already have NNp as a hypothesis we can then derive CNpNNp.  Since Caa is a theorem, we can derive CNpNp.  Along with axiom 3 we can then obtain p.  
Thus, we can write...
1 CCaCbaCCabCaa from axiom 2
2 CaCba axiom 1
3 CCabCaa detachment 1, 2
4 CCaCbaCaa from 3
5 Caa detachment 4, 2
6  | NNa hypothesis
7  | CNNaCNaNNa axiom 1
8  | CNaNNa detachment 7, 6
9  | CNaNa from 5
10 | CCNaNaCCNaNNaa axiom 3
11 | CCNaNNaa detachment 10, 9
12 | a  detachment 11, 8
13 CNNaa conditional introduction 6-12
14 | Cpq assumption
15 | Nq  assumption
16 || NNp hypothesis
17 || CNNpp by 13
18 || p  detachment 17, 16
19 || q  detachment 14, 18
20 | CNNpq conditional introduction 16-19
21 | CNqCNNpNq by axiom 1
22 | CNNpNq detachment 21, 15
23 | CCNNpqCCNNpNqNp by axiom 3
24 | CCNNpNqNp detachment 23, 20
25 | Np 24, 22 detachment

Note that this has 7 lines in the first part which need discharged and 4 lines in the second part which need discharged.  So, we have {[3(7)+2]+[3(4)+2]}=37 lines to write if we use the strictest proof of the deduction metatheorem.  With some pre-processing, and maybe also using condensed detachment, this can get considerably shortened.  In fact, I found that you can write a proof of CCpqCNqNp in this system using just 27 condensed detachments (which makes for a 30 line proof if you list the axioms also).
A: Combining the subformula strategy, weighting of the axioms, the assumptions, and the goal, and a (partial) level saturation search, I've found a 20 step (excluding the axioms and assumptions), level 6 proof using OTTER [1] (OTTER treats "p" and "q" here as nullary functions or in other words, constants).  
axiom             4 CxCyx.                  level 0
axiom             5 CCxCyzCCxyCxz.          0
axiom             6 CCNxyCCNxNyx.           0
assumption        7 Cpq                     0
assumption        8 Nq                      0
D4.4              9 CxCyCzy                 1
D5.5             10 CCCxCyzCxyCCxCyzCxz     1
D4.5             11 CxCCyCzuCCyzCyu         1
D5.4             12 CCxyCxx                 1
D5.6             13 CCCNxyCNxNyCCNxyx       1
D4.7             15 CxCpq                   1
D4.8             16 CxNq                    1
D4.9             19 CxCyCzCuz               2
DD5.5.9          20 CCxCCyxzCxz             2
DD5.4.4          27 Cxx                     2
D5.15            33 CCxpCxq                 2
D4.16            36 CxCyNq                  2
DD5.5.19         47 CCxCCyCzyuCxu           3
D20.11           50 CCxyCCzxCzy             3
D6.27            66 CCNxNNxx                3
DD5.6.36         95 CCNxqx                  3
D47.50          163 CCCxyzCyz               4
DD5.15.66       211 CCNpNNpq                4
D163.211        910 CNNpq                   5
D95.910        6213 Np                      6

[1]- W. McCune, "OTTER and Mace2", http://www.mcs.anl.gov/research/projects/AR/otter/, 1988-2014.
