I need to prove this natural deduction theorem:
$\neg \exists x.\neg \forall y.S_{1}^{1}(x) \implies S_{2}^{1}(y) \lor S_{3}^{1}(y)$, $S_{1}^{1}(c_1)$, $\neg S_{2}^{1}(c_2)$ $\vdash_{N} \exists z. S_{3}^{1}(z)$.
I understand how natural deduction works. However, I'm having some trouble understanding how to handle the quantifier's negations. I'm not sure if I should use equivalence rules (I mean, is that valid in natural deduction?) for the quantifiers to get rid of them.
Can you help me? Thanks in advance.