A metatheorem in mathematical logic also known under the name "conditional proof." It states that if the sentential
formula
can be derived from the set of sentential formulas
, then the sentential
formula
can be derived from
.
In a less formal setting, this means that if a thesis can be proven under the hypotheses
, then one can prove that
implies
under hypothesis
.