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