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