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