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