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