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