Consider the following premises. John is not running. If John goes running, then John is playing a game. For all x, x will go running or x will not play a game. Can we infer the following from them? If we can, name the inference rule being used: John is not playing a game.
 From the fact that for all x, x will go running or x will not play a game we can infer that for all x, if x plays a game, then x is running via universal rewriting. From the fact that for all x, if x plays a game, then x is running we can infer that if John plays a game, then John is running via universal instantiation. From the fact that if John goes running, then John is playing a game, and that if John plays a game, then John is running we can infer that John is running if and only if John is playing a game via biconditional introduction. Finally, from the fact that John is running if and only if John is playing a game, and that John is not running we can infer that John is not playing a game via biconditional elimination. Therefore, the answer is yes.