Consider the following premises. r <-> s. ~r. p_12 -> ~p_2. p_2. Can we infer ~s and ~p_12 from them? If possible, name the inference rules being used at each step.
 From r <-> s we can infer s -> r via biconditional elimination. From p_12 -> ~p_2, p_2 we can infer ~p_12 via modus tollens. From s -> r, ~r we can infer ~s via modus tollens. Finally, from ~s, ~p_12 we can infer ~s and ~p_12 via conjunction. Therefore, the answer is yes.