Rule of inference - Biconditional proposition

I'm having trouble with one of the questions given as an assignment which is to prove: $$(p\land q)\leftrightarrow(r\land s), \neg r\land q \vdash \neg p$$

I guess I should use proof by contradiction starting with 'assuming $p$'. I haven't really seen biconditional proposition from textbook examples and I can't even find one.

Using biconditional elimination, $$(p\land q)\leftrightarrow(r\land s)$$

is logically equivalent to $$\big((p\land q)\to(r\land s)\big)\land\big((r\land s)\to(p\land q)\big)$$

I can't step forward to next step.

• Without some reference for while rules of inference you are using, this question can't be answered. The most obvious answer is "truth table", or you could infer $r = \bot$ and $q = \top$ from the second statement. – DanielV May 3 '15 at 1:39
• Assuming $p$ works ... Unpack the biconditional in first premise and derive $\lnot r$ and $q$ from 2nd premise by $\land$-elimination. Now, with $p$ and $q$, derive $p \land q$ by $\land$-intro and derive $r \land s$ by $\to$-elimination. Now apply again $\land$-elim to derive $r$. Having $r$ and $\lnot r$ we can conclude with the negation of the assumption, i.e. $\lnot p$. – Mauro ALLEGRANZA May 3 '15 at 19:21

Possible sketch for a proof, where $\Sigma=\left\{(p\land q)\leftrightarrow(r\land s),(\neg r\land q)\right\}$:
1. $(p\land q)\leftrightarrow(r\land s)\vdash(p\land q)\to(r\land s)$ $\quad$ [$\leftrightarrow$-elimination]
2. $\neg r\land q\vdash\neg r$ $\quad$ [$\land$-elimination]
3. $\Sigma\vdash\neg r\lor\neg s$ $\quad$ [$\lor$-introduction 2]
4. $\Sigma\vdash\neg(r\land s)$ $\quad$ [De Morgan 3]
5. $\Sigma\vdash\neg(r\land s)\to\neg(p\land q)$ $\quad$ [Contrapositive 1]
6. $\Sigma\vdash\neg(p\land q)$ $\quad$ [Modus Ponens 4-5]
7. $\Sigma\vdash\neg p\lor\neg q$ $\quad$ [De Morgan 6]
8. $\neg r\land q\vdash q$ $\quad$ [$\land$-elimination]
9. $\Sigma\vdash\neg p$ $\quad$ [Disjunction 7-8]