Consider the following premises. ~s_1. p_13 <-> t_3. s_1 or t_3. Can we infer p_13 from them? If possible, name the inference rules being used at each step.
 From p_13 <-> t_3 we can infer t_3 -> p_13 via biconditional elimination. From s_1 or t_3, ~s_1 we can infer t_3 via disjunctive syllogism. Finally, from t_3 -> p_13, t_3 we can infer p_13 via modus ponens. Therefore, the answer is yes.