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