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