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