Consider the following premises. For all y, if y were a taxi driver, then y is writing a letter. For all y, if y writes a letter, then y is a taxi driver. Charles is writing a letter. Can we infer the following from them? If we can, name the inference rule being used: Charles is not a taxi driver.
 From the fact that for all y, if y were a taxi driver, then y is writing a letter, and that for all y, if y writes a letter, then y is a taxi driver we can infer that for all y, y is a taxi driver if and only if y will write a letter via universal biconditional introduction. From the fact that for all y, y is a taxi driver if and only if y will write a letter we can infer that Charles is a taxi driver if and only if Charles is writing a letter via universal instantiation. From the fact that Charles is a taxi driver if and only if Charles is writing a letter we can infer that if Charles writes a letter, then Charles is a taxi driver via biconditional elimination. Finally, from the fact that if Charles writes a letter, then Charles is a taxi driver, and that Charles is writing a letter we can infer that Charles is a taxi driver via modus ponens, which contradicts that Charles is not a taxi driver. Therefore, the answer is no.