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