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