Formal deductions on Hilbert system I have proved {(α→β),(β →γ)}  ⊢ (α→γ) } using formal deductions using Modus Ponens and the three axiom of H2 : 
A1: A -> (B-> A)
A2: (A-> (B->C)) -> ((A-> B) -> ( A -> C)) 
A3: (( ¬ A) -> ( ¬B)) -> ( B -> A) 
However now my professor is asking me to prove : 
 (1) (α→β) ⊢ (β →γ)→(α→γ)
and (2) ⊢ (α→β)->((β →γ)→(α→γ)). I am stuck on it since proving their existence with the deduction theorem is not enough. I must use formal deductions, any help for this ? Thank you
 A: OK, let's call your first proven pattern HS (for Hypothetical Syllogism).  We can nicely exploit that one for the next two. First, let's prove $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$:


*

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

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

*$(B \rightarrow C) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$  HS 1,2

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

*$((B \rightarrow C) \rightarrow (A \rightarrow B)) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ MP 3,4

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

*$(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ HS 5,6
This makes the proof of $\vdash (B \rightarrow C) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ trivial:


*

*$A \rightarrow B$ Assumption

*$(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ (we just proved this)

*$(B \rightarrow C) \rightarrow (A \rightarrow C)$ MP 1,2
