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