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