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