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