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