Consider the following premises. p_13 <-> q_13. p_4 -> p_13. q_13 or p_4. Can we infer p_13 or t_1 from them? If possible, name the inference rules being used at each step.
 From p_13 <-> q_13 we can infer q_13 -> p_13 via biconditional elimination. From q_13 -> p_13, p_4 -> p_13, q_13 or p_4 we can infer p_13 via disjunction elimination. Finally, from p_13 we can infer p_13 or t_1 via addition. Therefore, the answer is yes.