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