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.
 A: 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!
A: We have to prove :

$(∀xϕ(x)→ψ) \rightarrow ∃x(ϕ(x)→ψ)$ 

using Natural Deduction without "abbreviations".

Proof :
1) $\phi(x)$ --- assumed [1]
2) $\lnot \phi(x)$ --- assumed [2]
3) $\bot$ --- 1), 2) : $\rightarrow$E
4) $\psi$ --- 3) : $\bot$E
5) $\phi(x) \rightarrow \psi$ --- 1) and 4) : $\rightarrow$I, discharging [1]
6) $\exists x(\phi(x) \rightarrow \psi)$ --- 5) : $\exists$I
7) $\lnot \exists x(\phi(x) \rightarrow \psi)$ --- assumed [3]
8) $\bot$ --- 6), 7) : $\rightarrow$E
9) $\phi(x)$ --- 2), 8) : RAA, discharging [2]
10) $\forall \phi(x)$ --- 9) : $\forall$I
11) $\forall \phi(x) \rightarrow \psi$ --- assumed [4]
12) $\psi$ --- 10), 11) : $\rightarrow$E
13) $\phi(x) \rightarrow \psi$ --- 12) : $\rightarrow$I
14) $\exists x(\phi(x) \rightarrow \psi)$ --- 13) : $\exists$I
15) $\bot$ --- 14), 7) : $\rightarrow$E
16) $\exists x(\phi(x) \rightarrow \psi)$ --- 7), 15) : RAA, discharging [3]


$\vdash (∀xϕ(x)→ψ) \rightarrow \exists x(\phi(x) \rightarrow \psi)$ --- 1), 16) : $\rightarrow$I



Notes
A) In the above proof we have only one application of $\forall$I (step 10); in that step, the only undischarged assumption is [3], where $x$ is not free. Thus, contrary to the other "direction", the proviso : $x \notin FV(\psi)$ is not necessary.
B) In the derivation we have used RAA: this use is essential, as shown by the fact that : $(∀xϕ(x)→ψ) \rightarrow ∃x(ϕ(x)→ψ)$ is not intuitionistically valid.
A: 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.
