Hilbert Calculus statement proof I want to prove in $HPC$ that 
$$ \vdash_{HPC} (A\rightarrow B)\rightarrow ((B\rightarrow C) \rightarrow (A\rightarrow C ))$$
I tried using different combinations of the $A\rightarrow (B \rightarrow A)$ and 
$ (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) $ axioms but didn't reach the result. What am I missing?
thanks.
 A: Solution:
Using the deduction theorem for $HPC$, this is correct iff:
$$ A\rightarrow B, B \rightarrow C, A \vdash_{HPC} C$$
which is easily proven by using the $MP$ rule 2 times.
A: I use Polish notation.  This means that well-formed formulas get re-defined such that every wff of the form ($\alpha$$\rightarrow$$\beta$) gets translated to C$\alpha$$\beta$.  I don't spell out the substitutions made in the below, but I use spacing to show that a substitution follows the form of the axiom.  The basic idea runs as follows: we prove CCbcCCabCac and then change the positions of 'Cbc' and 'Cab'.
1. CaCba axiom 
2. CCaCbcCCabCac axiom 
3. C CCaCbcCCabCac C Cbc CCaCbcCCabCac 1
4. CCbcCCaCbcCCabCac 3, 2
5. CC Cbc C CaCbc CCabCac CC Cbc CaCbc C Cbc CCabCac 2
6. CCCbcCaCbcCCbcCCabCac 5, 4
7. C Cbc C a Cbc 1
8. CCbcCCabCac 6, 7
9. CC Cbc C Cab Cac CC Cbc Cab C Cbc Cac 2
10. CCCbcCabCCbcCac 9, 8
11. C CCCbcCabCCbcCac C Cab CCCbcCabCCbcCac 2
12. CCabCCCbcCabCCbcCac 11, 10
13. CC Cab C CCbcCab CCbcCac CC Cab CCbcCab C Cab CCbcCac 2
14. CCCabCCbcCabCCabCCbcCac 13, 12
15. C Cab C Cbc Cab 1
16. CCabCCbcCac 14, 15

