Consider the following premises. u <-> r_1. ~u. forall x_1: ~P(x_1). u_1 <-> P(f). Can we infer ~u_1 and ~r_1 from them? If possible, name the inference rules being used at each step.
 From forall x_1: ~P(x_1) we can infer ~P(f) via universal instantiation. From u_1 <-> P(f), ~P(f) we can infer ~u_1 via biconditional elimination. From u <-> r_1, ~u we can infer ~r_1 via biconditional elimination. Finally, from ~u_1, ~r_1 we can infer ~u_1 and ~r_1 via conjunction. Therefore, the answer is yes.