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