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