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