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