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