Converse of Deduction Theorem

Question

I have a basic question about natural deduction and deduction theorem. I learn from my textbook that the deduction theorem

$$\textit{If }\ \Gamma,A\vdash B,\ \textit{ then }\ \Gamma\vdash A\rightarrow B.$$

corresponds to the introduction rule of $\rightarrow$ in natural deduction. This is trivially in fact. But what about the converse?

$$\textit{If }\ \Gamma\vdash A\rightarrow B,\ \textit{ then }\ \Gamma,A\vdash B.$$

It also holds. But what does it correspond to in natural deduction? Or how is it expressed in natural deduction?

It seems to me that the elimination rule of $\rightarrow$ does similar work, but it's different from the converse of the deduction theorem.

Thanks!

Answer 1

Yes, it is just a quick consequence of the elimination rule.

$\to $ Elimination (in its most common phrasing) says that if $\Gamma\vdash A\to B$ and $\Gamma\vdash A$ then $\Gamma\vdash B.$

So, if $\Gamma\vdash A\to B,$ then $\Gamma, A\vdash A\to B.$ And of course $\Gamma,A\vdash A,$ so applying the elimination rule gives $\Gamma,A\vdash B.$