deduction theorem

{{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 <math> P, A \vdash C</math> to an inference of the form <math> P \vdash A \rightarrow C </math> or vice versa, where <math>\vdash</math> is the turnstile symbol. The validity of the procedure is a metatheorem of the given logical theory.