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