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