Consider the following premises. If it is overcast, then Thomas is happy. It is overcast if and only if it is sunny. If Thomas were happy, then it is overcast. It is not sunny. Can we infer the following from them? If we can, name the inference rule being used: Thomas is not happy.
 From the fact that it is overcast if and only if it is sunny, and that it is not sunny we can infer that it is not overcast via biconditional elimination. From the fact that if Thomas were happy, then it is overcast, and that if it is overcast, then Thomas is happy we can infer that Thomas is happy if and only if it is overcast via biconditional introduction. Finally, from the fact that Thomas is happy if and only if it is overcast, and that it is not overcast we can infer that Thomas is not happy via biconditional elimination. Therefore, the answer is yes.