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