Consider the following premises. ~s <-> q. ~q_7. s -> q_7. Can we infer q from them? If possible, name the inference rules being used at each step.
 From s -> q_7, ~q_7 we can infer ~s via modus tollens. From ~s <-> q we can infer ~s -> q via biconditional elimination. Finally, from ~s -> q, ~s we can infer q via modus ponens. Therefore, the answer is yes.