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