Consider the following premises. r -> s. u or ~w. r <-> u. Can we infer w -> s from them? If possible, name the inference rules being used at each step.
 From r <-> u we can infer u -> r via biconditional elimination. From u or ~w we can infer w -> u via rewriting. From u -> r, r -> s we can infer u -> s via transitivity. Finally, from w -> u, u -> s we can infer w -> s via transitivity. Therefore, the answer is yes.