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