Proving $\forall x[p\vee\Phi(x)]\Longleftrightarrow [p\vee\forall x[\Phi(x)]$, where $p$ does not contain $x$ as a free variable

Your above effort is almost done to prove the equivalence for both directions, you only need to additionally realize $\forall xp\vee\forall \Phi(x) \implies \forall x[p\vee\Phi(x)]$ actually can be strengthened to $\forall xp\vee\forall \Phi(x) \Longleftrightarrow \forall x[p\vee\Phi(x)]$ when $p$ has no free occurrence of $x$. Also note in FOL the above equivalence with disjunction form doesn't hold in general, but its conjunction form always holds.

When formula $p$ has no free occurrence of $x$, $\forall x[p\vee\Phi(x)]$ is true if $p$ is true (which doesn't depend on $x$), or if $\forall x \Phi(x)$ is true, or both are true. So it's easy to check that this imposes the same truth conditions on both $p\vee\forall \Phi(x)$ and $\forall xp\vee\forall \Phi(x)$. Formally you can use $\forall$-elim, $\lor$-elim, and $\forall$-intro rules to syntactically derive if you can use a natural deduction system or similar rules in a Hilbert system.