Deduction Theorem

If there is a proof of $B$ that uses a formula $A$ as a premise, then there is a proof of the implication $A\to B$ that does not use $A$ as a premise. Formally:

$$\mathcal{S}\cup \{A\}⊢B⟺\mathcal{S}⊢A\to B$$

If we consider the special case when $\mathcal{S}$ is empty, this becomes $\{A⊢B\}⟺⊢A\to B$. Essentially, we are saying proving $B$ follows from $A$ is equivalent to proving that $A\to B$ is a tautology.