Formal proof of the statement Given two formulae $\varphi $ and $\varphi '$, how does one formally prove the following statement?
$$\forall x (\varphi (x)\wedge \varphi'(x))\equiv \forall y \varphi (y)\wedge \forall z \varphi'(z)$$
 A: I don't know if this up to your standards of rigor, but here's how I'd do it.
Remark. If you truly want a "formal proof," you'll need to specify what deductive system you're working in. Anyway, what follows is what I'd call a "rigorous, informal proof."
$(\Longrightarrow)$ Suppose $\forall x[\phi(x) \wedge \phi'(x)].$

Let $x$ be arbitrary.

Then $\phi(x) \wedge \phi'(x)$.
Thus $\phi(x)$, and also $\phi'(x)$.

Since we have shown $\phi(x)$ under the assumption that $x$ is arbitrary, we may conclude $\forall x \phi(x)$. Similarly, we may conclude $\forall x \phi'(x)$. Thus
$$\forall x \phi(x) \wedge \forall x \phi'(x)$$
as required.
$(\Longleftarrow)$ Suppose $\forall x \phi(x) \wedge \forall x \phi'(x)$. Thus
$$[1] \quad \forall x \phi(x)$$
$$[2] \quad \forall x \phi'(x)$$

Let $x$ be arbitrary.

Then by [1], we have $\phi(x)$.
And by [2], we have $\phi'(x)$.
Thus $\phi(x) \wedge \phi'(x)$.

Since we have shown $\phi(x) \wedge \phi'(x)$ under the assumption that $x$ is arbitrary, we may conclude that $$\forall x[\phi(x) \wedge \phi'(x)]$$
as required.
