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