**Deduction theorem** is a basic rule of inference in logic by which a conditional is formed out of an implication. The deduction theorem is also known as the **conditional introduction** rule of inference (or →I), and explains that if "P implies Q", then "if P then Q" is also true.

Addition may be formally presented as follows:

**(α β) α → β**

When constructing a proof of some formula, one may have to invoke the deduction theorem by means of an assumption. To do this, an assumption for conditional proof (ACP) α is created to show that if α is true, then β is true.

…

RTP α → β

α ACP

RTP Contradiction

…

β

α → β →I

In this setup, the subproof (by which α is assumed and β is demonstrated as following from α) satisfies the implication, which can be used to form a conditional.