If $x$ does not freely occur in $Φ,$ and $\:Φ, ϕ\: ⊨ ψ,$ then $\:Φ, ∀x\,ϕ\: ⊨ ∀x\,ψ ?$ Below is my proof (I don't know whether it is correct) of $$\text{if }ϕ ⊨ ψ,\text{ then }∀x\,ϕ ⊨ ∀x\,ψ.$$

Given J. Assume that $⟦∀x\,ϕ⟧_J=T$.
Given a in J’s domain, $⟦ψ⟧_(J[x↦a])=T$ because

$⟦ ϕ⟧_(J[x↦a])=T$
$ϕ ⊨ ψ$

So $⟦∀x\,ψ⟧_J=T$. QED.

Given the above result, and that $\:Φ, ϕ\: ⊨ ψ,$ and that $x$ does not freely occur in $Φ,$ what is the procedure to prove that $$Φ, ∀x\,ϕ\: ⊨ ∀x\,ψ ?$$
 A: *

*

Below is my proof (I don't know whether it is correct) of $$\text{if }ϕ ⊨ ψ,\text{ then }∀x\,ϕ ⊨ ∀x\,ψ.\tag{*}$$

I suspect that you are using the symbol $⊨$ to mean that $\to$ is
true instead of its usual, stronger meaning that $\to$ is a validity
(i.e., logically true). In any case, $(*)$ is at least as strong
as $$\big(ϕ ⊨ ψ\big)\implies\big(∀x\,ϕ {\implies} ∀x\,ψ\big),$$
which is invalid (i.e., false in some interpretation); so, $(*)$ is
also invalid.


*

Given the above result, and that $\:Φ, ϕ\: ⊨ ψ,$ and that $x$ does not freely occur in $Φ,$ what is the procedure to prove that $$Φ,
∀x\,ϕ\: ⊨ ∀x\,ψ ?$$

Summarising and relabelling for ease of reading: our premises are

*

*$\big(Fx \to Sx\big)\to\big(∀x\,Fx \to ∀x\,Sx\big)$

*$\big(P\land Fx\big)  \to Sx$

*$P \land ∀x\,Fx,$
and our conclusion is

*

*$∀x\,Sx.$
Here's an informal proof:
\begin{align} &&\big[\big(Fx \to Sx\big)\to\big(∀x\,Fx \to
∀x\,Sx\big)\big] \land \big[\big(P\land Fx\big)  \to
Sx\big]\land\big[P \land ∀x\,Fx\big] \\&\equiv &\big[\big(\big(Fx
\to Sx\big) \land ∀x\,Fx\big) \to ∀x\,Sx\big] \land
\big[\big(\big(P\land Fx\big)  \to Sx\big)\land \big(P \land
Fx\big)\big]\land\big[ ∀x\,Fx\big] \\&⊨ &\big[\big(\big(Fx \to
Sx\big) \land ∀x\,Fx\big) \to ∀x\,Sx\big] \land
\big[Sx\big]\land\big[ ∀x\,Fx\big] \\&⊨ &\big[\big(Sx \land
∀x\,Fx\big) \to ∀x\,Sx\big] \land \big[Sx\big]\land\big[ ∀x\,Fx\big]
\\&⊨ &∀x\,Sx. \end{align}
