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