Consider the following premises. r or r_4. r <-> p. p or ~r_4. Can we infer ~p from them? If possible, name the inference rules being used at each step.
 From r <-> p we can infer r -> p via biconditional elimination. From p or ~r_4 we can infer r_4 -> p via rewriting. Finally, from r -> p, r_4 -> p, r or r_4 we can infer p via disjunction elimination, which contradicts ~p. Therefore, the answer is no.