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