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