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