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