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