Consider the following premises. For all x_17, if x_17 were sad, then x_17 is running. If Charles goes running, then Karen is reading a book. Charles is not sad. Karen is reading a book if and only if Charles is sad. Can we infer the following from them? If we can, name the inference rule being used: Karen is not reading a book.
 From the fact that for all x_17, if x_17 were sad, then x_17 is running we can infer that if Charles were sad, then Charles is running via universal instantiation. From the fact that Karen is reading a book if and only if Charles is sad we can infer that if Karen reads a book, then Charles is sad via biconditional elimination. From the fact that if Charles were sad, then Charles is running, and that if Charles goes running, then Karen is reading a book we can infer that if Charles were sad, then Karen is reading a book via transitivity. From the fact that if Karen reads a book, then Charles is sad, and that if Charles were sad, then Karen is reading a book we can infer that Karen is reading a book if and only if Charles is sad via biconditional introduction. Finally, from the fact that Karen is reading a book if and only if Charles is sad, and that Charles is not sad we can infer that Karen is not reading a book via biconditional elimination. Therefore, the answer is yes.