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