deduction theorem

Noun

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