Are these predicate formulas equivalent? Are these first-order formulas equivalent?
$$(\forall x)[(Ax \to Bx)\to(Cx \to Dx)]\tag{1}$$
$$(\forall x)(Ax \to Bx)\to (\forall x)(Cx \to Dx)\tag{2}$$
$$(\forall x)(Ax \to Bx)\to (\forall y)(Cy \to Dy)\tag{3}$$
I think (2) and (3) are equivalent, but I am not sure about (1).
 A: Here's a counterexample that shows (1) is not equivalent to (2): Let the universe be $\{1,2,3,4\}$, and let $Ax$ mean $x=1$, $Bx$ mean $x=2$, $Cx$ mean $x=3$, and $Dx$ mean $x=4$.
I will let you compute the truth values of the formulas in this interpretation. This is fairly quick to do with truth tables because the universe is small and finite, and is a good exercise if these matters are not clear to you.
Also, doing this concrete computation for (2) and (3) should give you an intuitive feeling for why they are necessarily equivalent.
A: $(1)$ has the schema $\forall x~(\psi\to\varphi)$ while $(2)$ has the schema $(\forall x~\psi)\to(\forall x~\varphi)$.   Now while the former logically entails the latter the converse does not hold.
Consider a universe where $\exists x~\lnot\psi$ and $\exists x~(\psi\land\lnot\varphi)$ are facts.

$(3)$ has te schema $(\forall x~\psi)\to(\forall y~{\psi\vert}^x_y)$.   If $y$ does not occur freely withing $\psi$, then $(2)$ and $(3)$ will be logically equivalent.
