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