How would I do a derivation of this: ¬q→(q↔r), ¬q∧(p∨r) ⊢ p using inference rules?

Question

I'm having a lot of trouble figuring out how to construct a derivation of

¬q→(q↔r), ¬q∧(p∨r) ⊢ p

So far I've used conjunction elimination to get (p∨r) but then this is where I get stuck.

I'm supposed to use disjunction elimination to get to p but I'm having trouble figuring out where to use it.

I'm allowed to use

∧Intro, ∨Intro, ¬Intro, →Intro, ↔Intro, ∧Elim, ∨Elim, ¬Elim, →Elim, and ↔Elim

inference rules.

Help!

Answer 1

I'm not going to piece together exactly what rules to use and when, but here's the outline. Like you say, the conjunction gives you $p\lor r,$ and also gives you $\lnot q.$ Since you have $\lnot q$ and $\lnot q\to (q\leftrightarrow r),$ you obtain $(q\leftrightarrow r).$ Then proceed toward disjunction elimination on $p\lor r.$ In the case where you have $p,$ you obviously have $p$. In the case where you have $r,$ you can use $q\leftrightarrow r$ to obtain $q.$ However, you have $\lnot q,$ so a contradiction, and so you have anything you want, including $p.$

(Most of the steps of the reasoning map straightforwardly to inference rules. The very last step might require a bit of unpacking since you aren't working in a system where ex-falso is a fundamental rule. Just mimic whatever proof of ex-falso you were given that works in your system to derive $p$.)