Consider the following premises. Robert is working if and only if John is a bartender. For all x_7, x_7 will read a book. For all x_7, if x_7 works, then x_7 is not reading a book. Can we infer the following from them? If we can, name the inference rule being used: John is not a bartender.
 From the fact that for all x_7, if x_7 works, then x_7 is not reading a book, and that for all x_7, x_7 will read a book we can infer that for all x_7, x_7 will not work via universal modus tollens. From the fact that for all x_7, x_7 will not work we can infer that Robert is not working via universal instantiation. Finally, from the fact that Robert is working if and only if John is a bartender, and that Robert is not working we can infer that John is not a bartender via biconditional elimination. Therefore, the answer is yes.