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