LEQV = Logically equivalent

I need help changing

∀xA(x) ^ ∀xB(x) ^ ∀xC(x) → ∀xD(x)

into PNF (such that the only connectives in the quantifier free portion have to be →)

∀xA(x) ^ ∀xB(x) ^ ∀xC(x) → ∀xD(x)

LEQV

￢ ( ∀xA(x) ^ ∀xB(x) ^ ∀xC(x) ) v ∀xD(x) [→ Law]

LEQV

( ∃x￢A(x) v ∃x￢B(x) v ∃x￢C(x) ) v ∀xD(x) [Duality of quantifiers law]

LEQV

∃x1∃x2∃x3∀x ( ( ￢A(x1) v ￢B(x2) v ￢C(x3) ) v D(x) ) [pulling quantifiers out]

LEQV

∃x1∃x2∃x3∀x ( ￢ ( A(x1) ^ B(x2) ^ C(x3) ) v D(x) ) [pulling￢ out]

LEQV

∃x1∃x2∃x3∀x ( ( A(x1) ^ B(x2) ^ C(x3) ) → D(x) ) [reverse → Law ]

I got here but I need the only connectives in the quantifier free portion to be →, right now the last step includes ^ symbols...

Thanks