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