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