Natural deduction proof of $(c ∧ n) → t, h ∧ ¬s, h ∧ ¬(s ∨ c) → p \vdash (n ∧ ¬t) → p$

Question

I'm trying to do a question from Huth and Ryan's book Logic in Computer Science and I am stuck on the following natural deduction proof:

Prove by natural deduction that the sequent

$$(c ∧ n) → t, h ∧ ¬s, h ∧ ¬(s ∨ c) → p \vdash (n ∧ ¬t) → p$$

is valid.

I have tried assuming $n ∧ ¬t$ on line 4 after the premises, and using Modus Tollens from there to get $¬(c ∧ n)$, but I don't know what I can do after that. Any help would be appreciated.

Answer 1

$\begin{align}n, \neg (c\wedge n)\vdash&~ \neg c \\ h\wedge \neg s\vdash&~ \neg s \\ h\wedge \neg s\vdash&~ h \\ \neg c, \neg s\vdash&~ \neg (s\vee c)\\ h, \neg(s\vee c), h\wedge \neg (s\vee c)\to p\vdash & ~ p\end{align}$

More or less. Format and provide justifications .