This question is from “Introduction to Mathematical Logic” by Elliot Mendelson , forth edition , page 75.
In page 75 of the book , there is a corollary in a paragraph that can be used to apply the Deduction Theorem multiple times in a row.
The new proof of $Gamma vdash mathscr B to mathscr C$ (in Proposition 2.4 $Gamma vdash mathscr C$ )
involves an application of Gen to a wf depending upon a wf $mathscr E$ of $Gamma$ only if
there is an application of Gen in the given proof of $Gamma, mathscr B vdash mathscr C$ that involves
the same quantified variable and is applied to a wf that depends upon $mathscr E$.
But there seems to be no justification/proof about this corollary.I searched online but non of them seem to mention this corollary.Are there any references about this I can read or is it just too trivial?
Here is an failed attempt of mine for justifying this corollary.
1.Technique for applying deduction multiple times in Mendelson Logic.