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