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