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