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