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