Consider the following premises. p -> u. u <-> w. Can we infer ~(p -> w) from them? If possible, name the inference rules being used at each step.
 From u <-> w we can infer u -> w via biconditional elimination. Finally, from p -> u, u -> w we can infer p -> w via transitivity, which contradicts ~(p -> w). Therefore, the answer is no.