Proof of transitivity in Hilbert Style We can use the following axioms:
$$\begin{align}
&A\to(B\to A)&\tag{A1}\\
&[A\to(B\to C)]\to[(A\to B)\to(A\to C)]&\tag{A2}\\
&(\lnot A\to\lnot B)\to(B\to A)&\tag{A3}
\end{align}$$
We need to prove: $$A\to B, B\to C\vdash A\to C$$
The hint is to use The Deduction Theorem.
I can't for the love of me figure it out, please help :(
 A: I assume you can use modus ponens as a deductive rule. Here is a Hilbert-style proof. As you can see, there is no reason to use the deduction theorem. 


*

*$A \to B$ [assumption]

*$B \to C$ [assumption]

*$(B \to C) \to (A \to (B \to C))$ [by A1]

*$A \to (B \to C)$ [modus ponens, 2 and 3]

*$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$ [by A2]

*$(A \to B) \to (A \to C)$ [modus ponens, 4 and 5]

*$A \to C$ [modus ponens, 1 and 6]

A: $$A \to B, B \to C \vdash A \to C$$
by deduction theorem
$$A \to B, B \to C, A \vdash C$$
applying $B \to C$
$$A \to B, A \vdash B$$
applying $A \to B$
$$A \vdash A$$
tautology.
A: If the deduction meta-theorem has an "if and only if" statement, then the deduction meta-theorem tells us that from 
"Cab, Cbc |-Cbc" we can obtain "Cab, Cbc, a|-c" by detachment and conversely (making the meta-logic into the object logic).  I call the part which enables us to move from "Cab, Cbc |-Cbc" to "Cab, Cbc, a|-c" The Detachment Meta-Theorem, and the other part The Deduction Meta-Theorem.  So far as I can tell, any metalogical proof of the deduction meta-theorem will necessarily tell us that we'll have modus ponens, so the detachment meta-theorem immediately holds even if not stated.  So, now, here's another proof:
 1 Cab premise
 2 Cbc premise
 3 a premise
 4 b 1, 3 modus ponens
 5 c 2, 4 modus ponens
 6 Cac 3-5 by Conditional Introduction.

Conditional Introduction comes as one of the rules of inference that The Deduction Meta-Theorem entails.
The Detachment Theorem, at least in my opinion, comes as MUCH more powerful and important than the Deduction Theorem, and it also comes as easier to metalogically argue for.  There do exist logical systems where the part of The Deduction Theorem that enables you to move from "{$\Gamma$, $\alpha$} $\vdash$ $\beta$" to "$\Gamma$ $\vdash$ C$\alpha$$\beta$" does not work, but you still have The Detachment Theorem.  On the other hand there do not exist logical systems where the part of The Deduction Theorem that enable you to move from "$\Gamma$ $\vdash$ C$\alpha$$\beta$" to "{$\Gamma$, $\alpha$} $\vdash$ $\beta$" does not work, but you still have the other half of The Deduction Theorem.  The only logical systems where The Detachment Theorem does not work consist of those systems where detachment is not a primitive or derivable rule of inference of the logical system.  In some sense, there exist "more" logical systems with The Detachment Meta-Theorem than the Deduction Meta-Theorem.
