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