Negation with multiple quantifiers

Question

I have a logical statement that looks like the following for the sentence "If every cat feels wet, then every dog is happy"

$$ [\forall x \ \ C(x) \implies W(x)] \implies [\forall y \ \ D(y) \implies H(y)] $$

I want to put the NEGATED version of this statement in CNF form, so first I remove all the implications: $$ \lnot([\forall x \ \ \lnot C(x) \lor W(x)] \implies [\forall y \ \ \lnot D(y) \lor H(y)]) \\ \lnot([\lnot\forall x \ \ \lnot C(x) \lor W(x)] \lor [\forall y \ \ \lnot D(y) \lor H(y)]) \\ \lnot([\exists x \ \ C(x) \land \lnot W(x)] \lor [\forall y \ \ \lnot D(y) \lor H(y)]) \ \ \ \text{used Demorgan's Law here}\\ $$

Assuming the above steps are current, I am confused on how to distribute the outermost negation inside when there are quantifiers and logical statements.

I understand the following conversions:

$$ \lnot \forall x \ P(x) = \exists x \ \lnot P(x) \\ \lnot \exists x \ P(x) = \forall x \ \lnot P(x) \\ \lnot (a \lor b \lor...c) = \lnot (\lnot a \land \lnot b \land...\lnot c) \\ \lnot (a \land b \land...c) = \lnot (\lnot a \land \lnot b \lor...\lnot c) $$

but it's not clear to me how I can distribute the outermost negation because now it involves quantifiers. Any hints?

Edit 1

I think I may have gotten it:

$$ (\lnot[\exists x \ \ C(x) \land \lnot W(x)] \land \lnot[\forall y \ \ \lnot D(y) \lor H(y)]) \\ ([\forall x \ \ \lnot C(x) \lor W(x)] \land [\exists y \ \ D(y) \land \lnot H(y)]) \\ $$

Answer 1

One extra substitution rule to remember is Implication Negation Equivalence: $$\neg(\phi\to\psi) ~\equiv~ (\phi\wedge\neg\psi)$$

This can be derived using:

$$\begin{align}\neg(\phi\to\psi)&\quad&\\\neg(\neg\phi\vee\psi)&&&\text{Implication Equivalence}\\\neg\neg\phi\wedge\neg\psi&&&\text{de Morgan's Rule}\\\phi\wedge\neg\psi&&&\text{Double Negation Equivalence}\end{align}$$

Also vice versa.

Thus your statement's negation begins:

$$\begin{align}&\neg\Big(\big(\forall x~(Cx\to Wx)\big)\to\big(\forall y~(Dy\to Hy)\big)\Big) \\&\quad\big(\forall x~(Cx\to Wx)\big)\wedge\neg\big(\forall y~(Dy\to Hy)\big)&&\text{Implication Negation Equivalence} \\&\quad\vdots\end{align}$$

And it should be clear how to continue.

---

Also recall that the distribution rules for quantifiers in non-empty domains includes: $$(\forall x~P(x))\wedge (\exists y~Q(y))~~\equiv~~ \forall x~\exists y~(P(x)\wedge Q(y))$$