How do the prenex conversion rules for conjunctions and disjunctions come from these logical axioms?

Question

Wikipedia states the following rules:

$(\forall x\phi )\land\psi$ is equivalent to $\forall x(\phi\land\psi )$ under (mild) condition ... that at least one individual exists),
$(\forall x\phi )\lor\psi$ is equivalent to $\forall x(\phi\lor\psi )$;

and

$(\exists x\phi )\land\psi$ is equivalent to $\exists x(\phi\land\psi )$,
$(\exists x\phi )\lor\psi$ is equivalent to $\exists x(\phi\lor\psi )$ under the additional condition [that there is an individual].

... $x$ does not appear as a free variable of $\psi$.

The logical axioms I’m concerned with are mentioned in Wolf’s A Tour Through Mathematical Logic, Appendix A A Deductive System for First-order Logic which Wolf claims to have taken from Enderton’s book. These are:

Logical axioms

The logical axioms are all generalisations of all formulas of the following types.

1. All tautologies.
2. Universal specification: $\forall xP(x)\rightarrow P(t)$, where $t$ is a term of the same sort as the variable $x$, $P(t)$ is the result of replacing all free occurrences of $x$ in $P(x)$ by $t$, and no free variable of $t$ becomes bound in $P(t)$.
3. $\forall x(P\rightarrow Q)\rightarrow (\forall xP\rightarrow\forall xQ)$.
4. $P\rightarrow\forall xP$, where $x$ does not occur free in $P$.
5. Definition of $\exists$: $\exists P\leftrightarrow\neg\forall x\neg P$.
6. $x=x$.
7. Substitution of equals: $x=y\rightarrow [P(x)\leftrightarrow P(y)]$, where $P$ is atomic and $P(y)$ is the result of replacing one or more occurrences of $x$ in $P(x)$ by $y$.

Rule of inference

1. Modus ponens: From two steps of the form $P$ and $P\rightarrow Q$, $Q$ may be concluded.

---

Question: How to deduce the above prenex rules from the above first-order logical deductive system?