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