In natural deduction accounts of proof theory, the act of absorbing an assumption by introducing it into the antecedent of a conditional at a later stage, where also has appeared. After a formula has been discharged, it may not be employed in further derivations. For example, a conditional proof of the classical theorem can be informally represented by the inference:
In the third step, the first premise is absorbed into the new conditional and that instance of the formula is discharged, as indicated by the bar over it.