Assumption discharge
= Assumption discharge
<Assumption discharge> closes a designated <temporary assumption> together with its dependent subproof. <Implication introduction rule> turns a <logical derivation> of $B$ under $A$ into $A\to B$ outside that temporary scope. <Negation introduction rule> turns a <logical derivation> of <logical falsity> under $A$ into $\neg A$. <Disjunction elimination rule> discharges its separate case assumptions while retaining any surrounding premises.