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