Consider the following premises. If John works, then Charles is cooking. Michael is not listening to a song. If Charles cooks, then Michael is listening to a song. If it rains, then John is working. If Michael listens to a song, then it is raining. Can we infer the following from them? If we can, name the inference rule being used: It is not raining.
 From the fact that if John works, then Charles is cooking, and that if Charles cooks, then Michael is listening to a song we can infer that if John works, then Michael is listening to a song via transitivity. From the fact that if it rains, then John is working, and that if John works, then Michael is listening to a song we can infer that if it rains, then Michael is listening to a song via transitivity. From the fact that if it rains, then Michael is listening to a song, and that if Michael listens to a song, then it is raining we can infer that it is raining if and only if Michael is listening to a song via biconditional introduction. Finally, from the fact that it is raining if and only if Michael is listening to a song, and that Michael is not listening to a song we can infer that it is not raining via biconditional elimination. Therefore, the answer is yes.