Consider the following premises. forall x_3: S_2(x_3) -> Q_1(x_3). Q_1(a_7) <-> q. forall x_3: Q_1(x_3) -> S_2(x_3). ~q. Can we infer ~S_2(a_7) from them? If possible, name the inference rules being used at each step.
 From forall x_3: S_2(x_3) -> Q_1(x_3), forall x_3: Q_1(x_3) -> S_2(x_3) we can infer forall x_3: S_2(x_3) <-> Q_1(x_3) via universal biconditional introduction. From forall x_3: S_2(x_3) <-> Q_1(x_3) we can infer S_2(a_7) <-> Q_1(a_7) via universal instantiation. From Q_1(a_7) <-> q, ~q we can infer ~Q_1(a_7) via biconditional elimination. Finally, from S_2(a_7) <-> Q_1(a_7), ~Q_1(a_7) we can infer ~S_2(a_7) via biconditional elimination. Therefore, the answer is yes.