= Weakening
{title2=$\Gamma\vdash A\implies\Gamma,\Delta\vdash A$}
Adding unused assumptions to the context of a <logical derivation>. The original derivation still proves the same conclusion because it need not use every available assumption. When <eigenvariables> are used, rename them first if necessary to preserve the <eigenvariable condition> for any newly added assumptions. This explains how <disjunction elimination> with different branch contexts can be written using a common context containing all their assumptions.
Back to article page
