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