Consider the following premises. For all y, if y were an office clerk, then y is writing a letter. It is overcast or Thomas is taking a plane. If it is overcast, then Charles is an office clerk. Charles is writing a letter if and only if Thomas is taking a plane. Can we infer the following from them? If we can, name the inference rule being used: Charles is writing a letter.
 From the fact that for all y, if y were an office clerk, then y is writing a letter we can infer that if Charles were an office clerk, then Charles is writing a letter via universal instantiation. From the fact that Charles is writing a letter if and only if Thomas is taking a plane we can infer that if Thomas takes a plane, then Charles is writing a letter via biconditional elimination. From the fact that if it is overcast, then Charles is an office clerk, and that if Charles were an office clerk, then Charles is writing a letter we can infer that if it is overcast, then Charles is writing a letter via transitivity. Finally, from the fact that if it is overcast, then Charles is writing a letter, that if Thomas takes a plane, then Charles is writing a letter, and that it is overcast or Thomas is taking a plane we can infer that Charles is writing a letter via disjunction elimination. Therefore, the answer is yes.