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