A metatheorem in mathematical logic also known under the name "conditional proof." It states that if the sentential formula B can be derived from the set of sentential formulas A_1, ..., A_n, then the sentential formula A_n ⟹B can be derived from A_1, ..., A_(n - 1). In a less formal setting, this means that if a thesis S can be proven under the hypotheses U, V, then one can prove that V implies S under hypothesis U.
