Consider the following premises. It is not sunny. If it rains, then Michael is playing a game. It is sunny if and only if it is raining. If Michael plays a game, then Thomas is excited. If Thomas were excited, then it is raining. Can we infer the following from them? If we can, name the inference rule being used: Thomas is not excited.
 From the fact that it is sunny if and only if it is raining, and that it is not sunny we can infer that it is not raining via biconditional elimination. From the fact that if it rains, then Michael is playing a game, and that if Michael plays a game, then Thomas is excited we can infer that if it rains, then Thomas is excited via transitivity. From the fact that if it rains, then Thomas is excited, and that if Thomas were excited, then it is raining we can infer that it is raining if and only if Thomas is excited via biconditional introduction. Finally, from the fact that it is raining if and only if Thomas is excited, and that it is not raining we can infer that Thomas is not excited via biconditional elimination. Therefore, the answer is yes.