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