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