Proof for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR I can't find a for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR
HR is the following system:
axioms:
$A\rightarrow A$
$(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow (A \rightarrow C))$
$(A\rightarrow (B\rightarrow C))\rightarrow (B\rightarrow (A\rightarrow C))$
$(A\rightarrow (A\rightarrow B))\rightarrow (A\rightarrow B)$
and the inference rule is MP.
I already proved that general claim that might help:
If $T,A\vdash B$ and $T\nvdash B$ than $T\vdash A\rightarrow B$
So here it's easy to prove that $\{p,p\rightarrow (q\rightarrow r),(p\rightarrow q)\}\vdash r$ , 
but I have know idea how to show that  $\{p,p\rightarrow (q\rightarrow r)\}\nvdash r$ 
 A: We assume that we do not have the resource of Deduction Theorem available.
(1) --- $p \rightarrow (q \rightarrow r)$ --- Assumption
(2) --- $p$ --- Assumption
(3) --- $(q \rightarrow r)$ --- from (1) and (2) by modus ponens
(4) --- $\vdash (p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r))$ --- Axiom 2
(5) --- $\vdash (q \rightarrow r) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$ --- from (4) and Axiom 3 by modus ponens
(6) --- $(p \rightarrow q) \rightarrow (p \rightarrow r)$ --- from (3) and (5) by modus ponens
Now we need the following form of Axiom 4 [$(A→(B→C))→(B→(A→C))$ - we use the substitution : $p \rightarrow q/A; p/B; r/C$ ] :

(7) --- $\vdash ((p \rightarrow q) \rightarrow (p \rightarrow r)) \rightarrow (p \rightarrow ((p \rightarrow q) \rightarrow r))$

(8) --- $p \rightarrow ((p \rightarrow q) \rightarrow r)$ --- from (6) and (7) by modus ponens
Now, it's done : apply modus ponens using the Assumption $p$, and we will get :


$(p \rightarrow q) \rightarrow r$.


The conclusion "depends" on the assumptions : $p$ and $p \rightarrow (q \rightarrow r)$.
A: Since Willemien thought it better to show that [p→((p→(q→r))→((p→q)→r))] is a theorem, I'll do that here.
I use Polish notation.
Your axioms are:
3 Cpp (weak law of identity)
4 CCpqCCqrCpr (syll or hypothetical syllogism)
5 CCpCqrCqCpr (commutation or "transposition")
6 CCpCpqCpq (contraction or Hilbert)
I use the notation Dx.y * z for condensed detachment with x as the major premise, y as the minor premise, and "z" as the resulting formula. I'll also write the annotation of the proof before the proof.
D4.4 * 8
 8 CCCCqrCprsCCpqs

D5.4 * 9
 9 CCqrCCpqCpr

D5.3 * 10
 10 CpCCpqq

D4.10 * 11
 11 CCCCpqqrCpr

D9.6 * 12
 12 CCrCpCpqCrCpq

D11.4 * 13
 13 CpCCqrCCpqr

D5.13 * 14
 14 CCpqCrCCrpq

D8.12 * 15
 15 CCpqCCqCprCpr

D5.15 * 16
 16 CCqCprCCpqCpr

D16.14 * 17
 17 CCrCpqCrCCrpq

D5.17 * 18
 18 CpCCpCqrCCpqr

Now we assume {p, CpCqr}.  By 18 and "p" we detach CCpCqrCCpqr.  From CpCqr and CCpCqrCCpqr we detach CCpqr.
