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