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