Consider the following premises. For all x_9, x_9 will work if and only if x_9 will play tennis. Thomas is not working. Can we infer the following from them? If we can, name the inference rule being used: Thomas is not playing tennis.
 From the fact that for all x_9, x_9 will work if and only if x_9 will play tennis we can infer that for all x_9, if x_9 plays tennis, then x_9 is working via universal biconditional elimination. From the fact that for all x_9, if x_9 plays tennis, then x_9 is working we can infer that if Thomas plays tennis, then Thomas is working via universal instantiation. Finally, from the fact that if Thomas plays tennis, then Thomas is working, and that Thomas is not working we can infer that Thomas is not playing tennis via modus tollens. Therefore, the answer is yes.