Deduction theorem for sentence assumptions

For each old line $\eta$ we construct a proof from $T$ of $\sigma \to \eta$, by induction along the finite list. If $\eta =\sigma$, use identity. If $\eta$ is an axiom or belongs to $T$, retain its one-line proof and apply the tautology $\eta \to (\sigma \to \eta )$ by MP. These include every possible first line.

If $\eta$ comes by MP from $\alpha$ and $\alpha \to \eta$, the already transformed premises and the tautology $(\sigma \to \alpha )\to ((\sigma \to (\alpha \to \eta ))\to (\sigma \to \eta ))$ give the new line by two MP applications.

If $\eta =\mathrm{\forall }x\alpha$ comes by generalization, generalize the transformed $\sigma \to \alpha$ to $\mathrm{\forall }x(\sigma \to \alpha )$, then use distribution to obtain $\sigma \to \mathrm{\forall }x\alpha$. Its restriction holds because $x$ is not free in $\sigma$.

If $\eta =(\mathrm{\exists }x\alpha \to \beta )$ comes from $\alpha \to \beta$, the transformed premise is $\sigma \to (\alpha \to \beta )$. Boolean commutation gives $\alpha \to (\sigma \to \beta )$. Eliminate $x$ to get $\mathrm{\exists }x\alpha \to (\sigma \to \beta )$, since $x$ is free in neither $\sigma$ nor $\beta$. Commute back to $\sigma \to (\mathrm{\exists }x\alpha \to \beta )$.

The three rule cases exhaust the list. Concatenating each finite derived block gives a finite proof of $\sigma \to \theta$ from $T$. For a sentence $\sigma$ both variable restrictions hold automatically. Conversely, weaken a proof of $\sigma \to \theta$ to $T\cup \{\sigma \}$, append its assumption $\sigma$ and apply MP to obtain $\theta$.