Équivalence logique entre trois énoncés

Bonjour à toutes et tous
J'ai une question un peu stupide.

Soit $\mathcal{L}$ un langage du premier. Soient $A(x)$ et $B(y,z)$ deux $\mathcal{L}$-formules dont les variables libres sont respectivement incluses dans $\{x\}$ et $\{y,z\}$.

Êtes-vous d'accord pour dire que les formules ci-dessous sont logiquement équivalentes ?

Formule n°1 : $[\forall x A(x)] \to [\forall z \exists y B(y,z)]$

Formule n°2 : $\forall z \exists x \exists y [A(x) \to B(y,z)]$

Formule n°3 : $\exists x \forall z \exists y [A(x) \to B(y,z)]$

J'ai démontré sémantiquement et assez simplement ces trois équivalences (pour les connaisseurs : à certains endroits la démonstration ressemble un peu à la preuve sémantique de la validité de la "formule du buveur").

Malgré tout, l'interversion des quantificateurs dans les formules n°2 et n°3 me semble suspect. Par conséquent, j'ai peur d'avoir fait une erreur grossière dans ma démonstration.

Merci d'avance pour vos réponses.

PS : Évidemment, pour toutes paires de $\mathcal{L}$-énoncés $\phi$ et $\psi$, on dit que $\phi$ et $\psi$ sont logiquement équivalentes lorsque $\vdash \phi \leftrightarrow \psi$.