Consider the following premises. forall x_17: P_17(x_17) -> Q_17(x_17). forall x_17: Q_17(x_17) -> P_17(x_17). Q_17(a_7) -> ~u_1. t. t -> u_1. Can we infer ~P_17(a_7) from them? If possible, name the inference rules being used at each step.
 From forall x_17: P_17(x_17) -> Q_17(x_17), forall x_17: Q_17(x_17) -> P_17(x_17) we can infer forall x_17: P_17(x_17) <-> Q_17(x_17) via universal biconditional introduction. From t -> u_1, t we can infer u_1 via modus ponens. From forall x_17: P_17(x_17) <-> Q_17(x_17) we can infer P_17(a_7) <-> Q_17(a_7) via universal instantiation. From Q_17(a_7) -> ~u_1, u_1 we can infer ~Q_17(a_7) via modus tollens. Finally, from P_17(a_7) <-> Q_17(a_7), ~Q_17(a_7) we can infer ~P_17(a_7) via biconditional elimination. Therefore, the answer is yes.