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