# deduction theorem

1. (logic) A procedure for "discharging" assumptions from an inference, causing them to become antecedents of the conclusion; or vice versa. Symbolically, the conversion of an inference of the form ${\displaystyle P,A\vdash C}$ to an inference of the form ${\displaystyle P\vdash A\rightarrow C}$ or vice versa, where ${\displaystyle \vdash }$ is the turnstile symbol. The validity of the procedure is a metatheorem of the given logical theory.