Deduction theorem

In mathematical logic, the deduction theorem is a metatheorem of propositional and first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then deriving B from this assumption conjoined with known results. The deduction theorem explains why proofs of conditional sentences in mathematics are logically correct. Though it has seemed "obvious" to mathematicians literally for centuries that proving B from A conjoined with a set of theorems is tantamount to proving the implication A → B based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case.

The deduction theorem states that if a formula B is deducible from a set of assumptions ${\displaystyle \Delta \cup \{A\}}$, where A is a closed formula, then the implication A → B is deducible from ${\displaystyle \Delta }$. In symbols, ${\displaystyle \Delta \cup \{A\}\vdash B}$ implies ${\displaystyle \Delta \vdash A\to B}$. In the special case where ${\displaystyle \Delta \,}$ is the empty set, the deduction theorem shows that ${\displaystyle \{A\}\vdash B}$ implies ${\displaystyle \vdash A\to B}$.

...
Wikipedia