Prove $\exists_x(\phi(x) \rightarrow \psi) \iff (\forall_x\phi(x) \rightarrow \psi)$ using natural deduction I want to prove $\exists_x(\phi(x) \rightarrow \psi) \iff (\forall_x\phi(x) \rightarrow \psi)$ where $x \notin FV(\psi)$ using natural deduction method. I was able to prove implication from left to right:
$$
{\exists_x(\phi(x) \rightarrow \psi) ~~~~~~~~{{[\phi[t/x]\rightarrow \psi]~~~~~~~ {{[\forall_x\phi(x)]}\over{\phi[t/x]}}} \over {\psi}}}\over{\psi \over {\forall_x\phi(x) \rightarrow \psi}}
$$

but I am not able to prove implicatin from right to left. I would appreciate any help.
Arguing informally in natural deduction style, assume as premiss 


  $\forall x\phi(x) \to \psi$


Now remember that that is elementarily equivalent to


  $\neg\forall x\phi(x) \lor \psi$


So the obvious brute force proof strategy is to argue by cases. You need to show, first, that $\neg\forall x\phi(x)$ implies $\exists x(\phi(x) \to \psi)$. But we have


  $\neg\forall x\phi(x)\\ \exists x\neg\phi(x)\\ \quad|\quad \neg\phi(a)\\ \quad|\quad \phi(a) \to \psi \\ \quad|\quad \exists x(\phi(x) \to \psi) \\  \exists x(\phi(x) \to \psi) $


using existential quantifier elimination at the key step. And now you need to show that $\psi$ implies $\exists x(\phi(x) \to \psi)$. But that's easy, we just need to fill in the proof


  $\psi\\ \phi(a) \to \psi \\ \exists x(\phi(x) \to \psi) $


So put everything together and we are done, in this informal Fitch-style presentation.

It remains to massage the proof into your preferred tree layout: exercise!
Well, $\exists x \phi(x) \rightarrow \psi$ is not logically equivalent to $\forall x \phi(x) \rightarrow \psi$. If every $x$ has some property, certainly there exists an $x$ with that property. However, just because some $x$ has a property does not mean every $x$ has a property. 

Unless your domain of discourse has only one element.

Edit: or if $\phi(x)$ is always false.