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.
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.
