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