Does the Definition of a Formal Proof in Mendelson's Book Allow for the Use of Theorem/Derived Axiom Schema in Formal Proofs? The relevance of this question concerns deciding whether or not a sequence of well-formed formulas in a text will qualify as a formal proof.

Mendelson's Introduction to Mathematical Logic on p. 25 of the 5th edition reads when defining a formal system:

"There is a finite set R$_1$, ..., R$_n$ of relations among wfs, called rules of inference.  For each R$_i$, there is a unique positive integer j such that, for every set of j wfs and each wf B, one can effectively decide whether the given j wfs are in the relation R$_i$ to B, and, if so, B is said to follow from or to be a direct consequence of the given wfs by virtue of R$_i$.

A proof in L is a sequence B$_1$, ..., B$_k$ of wfs such that, for each i, either B$_i$ is an axiom of L or B$_i$ is a direct consequence of some of the preceding wfs in the sequence by virtue of one of the rules of inference of L.

A theorem of L is a wf B of L such that B is the last wf of some proof in L."

He then sets up a formal system, and describes a few others in the exercises, though those details don't matter to this question.  One of his references is S. C. Kleene's Introduction to MetaMatheamtics where on p. 82 Kleene writes:

"The relation of 'immediate consequence' is defined thus.  A formula is an immediate consequence of one or two other formulas, if it has the form shown below the line, while the other(s) have the form(s) shown above the line in 2, 9, 12."

2, in context, states a rule of modus ponens.  9 states a one premise universal quantifier rule, and 12 a one premise existential quantifier rule.  Kleene then explains his definition of a formal proof more in detail partially by referring to the notion of an immediate consequence.

The phrases 'immediate consequence' and 'direct consequence' both suggest to me that a substitution instance of a formal theorem would qualify as a formal theorem also, but re-reading those definitions suggests that I may have read into things.  That said though, other authors like Prior, Bergmann, Lukasiewicz, and papers I've seen, suggest that substitutions in theorems in axiomatic systems coheres with the definition of a formal proof (and soundness works out).  But, there's also something called The Pushback Lemma which sounds like it says that for any substitution and detachment proof where we have substitutions in the formal theorems, there can get found from that formal proof a formal proof which only has substitutions in the primitive axioms or first axiom schemata.

So, does Mendelson's definition forbid substitutions in theorems in formal proofs, or does it allow substitutions in a formal theorem?
By the very definition you gave, clearly a proof can only use the given rules of inference and hence cannot invoke theorems in the meta-system. A common meta-theorem is the deduction theorem, namely that $A \vdash B$ if and only if $\vdash A \to B$, which a proof in $L$ is not allowed to use. Similarly a proof in $L$ cannot invoke theorem schemas by definition. For instance you can prove that, given any binary predicate symbol $P$, if $L \vdash \exists x\ \forall y\ ( P(x,y) )$ then $L \vdash \forall y\ \exists x\ ( P(x,y) )$. But you cannot use it in a proof.
$
\def\prov{\square}
$

In general, unless the formal system $L$ includes some kind of meta-logic that allows you to use meta-theorems, a proof is literally a sequence of deductions using only the inference rules. It is dangerous to have too strong internal meta-logic, because if $L$ has decidable proof validity and interprets arithmetic then:


  If $L \vdash A$ then $L \vdash \prov_L A$, for every sentence $A$ over $L$.


But if $L$ is $Σ_1$-sound then it cannot have:


  (INVALID) $L \vdash A \to \square_L A$, for every sentence $A$ over $L$.


This is because any such $L$ has 'internal completeness' in the sense that, given any sentence $A$ over $L$, we have that $L$ proves "$\prov A \lor \prov \neg A$", which is a $Σ_1$-sentence and hence must be true for $\mathbb{N}$, and the witness can be decoded into a proof of either "$A$" or "$\neg A$" over $L$, which contradicts Godel's first incompleteness theorem.
It forbids substitutions in theorems in formal proofs (NO formal proofs exist in the book... not a single one).  But, that is not generally how the axiomatic method has gotten used historically speaking.