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