Consider the following premises. w_2. p_7 -> ~w_2. u_3 <-> r_1. p_7 <-> u_3. Can we infer r_1 from them? If possible, name the inference rules being used at each step.
 From p_7 -> ~w_2, w_2 we can infer ~p_7 via modus tollens. From p_7 <-> u_3, ~p_7 we can infer ~u_3 via biconditional elimination. Finally, from u_3 <-> r_1, ~u_3 we can infer ~r_1 via biconditional elimination, which contradicts r_1. Therefore, the answer is no.