Consider the following premises. s. u_2 -> s. s -> u_2. Can we infer u_2 from them? If possible, name the inference rules being used at each step.
 From u_2 -> s, s -> u_2 we can infer u_2 <-> s via biconditional introduction. From u_2 <-> s we can infer s -> u_2 via biconditional elimination. Finally, from s -> u_2, s we can infer u_2 via modus ponens. Therefore, the answer is yes.