Consider the following premises. If William were a doctor, then David is taking a plane. If David writes a letter, then William is a doctor. For all x_12, x_12 will take a plane if and only if x_12 will write a letter. Can we infer the following from them? If we can, name the inference rule being used: William is a doctor if and only if David is taking a plane.
 From the fact that for all x_12, x_12 will take a plane if and only if x_12 will write a letter we can infer that David is taking a plane if and only if David is writing a letter via universal instantiation. From the fact that David is taking a plane if and only if David is writing a letter we can infer that if David takes a plane, then David is writing a letter via biconditional elimination. From the fact that if David takes a plane, then David is writing a letter, and that if David writes a letter, then William is a doctor we can infer that if David takes a plane, then William is a doctor via transitivity. Finally, from the fact that if William were a doctor, then David is taking a plane, and that if David takes a plane, then William is a doctor we can infer that William is a doctor if and only if David is taking a plane via biconditional introduction. Therefore, the answer is yes.