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