Consider the following premises. u_2 -> t. q_11 <-> u_2. ~t. r_1 -> q_11. q_11 -> r_1. Can we infer ~r_1 from them? If possible, name the inference rules being used at each step.
 From r_1 -> q_11, q_11 -> r_1 we can infer r_1 <-> q_11 via biconditional introduction. From u_2 -> t, ~t we can infer ~u_2 via modus tollens. From q_11 <-> u_2, ~u_2 we can infer ~q_11 via biconditional elimination. Finally, from r_1 <-> q_11, ~q_11 we can infer ~r_1 via biconditional elimination. Therefore, the answer is yes.