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