Consider the following premises. If Charles listens to a song, then Richard is working. For all y, y will not listen to a song. If Richard works, then Charles is listening to a song. Can we infer the following from them? If we can, name the inference rule being used: Richard is not working.
 From the fact that for all y, y will not listen to a song we can infer that Charles is not listening to a song via universal instantiation. From the fact that if Richard works, then Charles is listening to a song, and that if Charles listens to a song, then Richard is working we can infer that Richard is working if and only if Charles is listening to a song via biconditional introduction. Finally, from the fact that Richard is working if and only if Charles is listening to a song, and that Charles is not listening to a song we can infer that Richard is not working via biconditional elimination. Therefore, the answer is yes.