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