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