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