# Shoenfield's Mathematical logic book Proof of Herbrand's Theorem

I have trouble understanding the first lemma proof of the Herbrand's theorem section of the book. The proof of the lemma starts with a closed existential formula A and proves that A is a theorem iff T[$$\neg$$ B] is inconsistent, where B is the matrix of A. Then it invokes the consistency theorem (which states that an open Theory T is inconsistent iff there is a quasi-tautology which is a disjunction of negations of instances of nonlogical axioms of T ) as a chain to prove the lemma. But to use that, shouldn't $$\neg$$ B be a non-logical axiom of T ? and this can't even be a case, since the lemma states that T is a theory with no nonlogical axioms.

Here's where i take a look at to help me understand the argument. In this proof the same technique is adopted.

Apply the consistency theorem to the theory $\mathbf{T[not B]}$ rather than to $\mathbf{T}$.