Consider the following premises. For all x_7, x_7 is fast or x_7 is not a poet. If David were fast, then David is a poet. Can we infer the following from them? If we can, name the inference rule being used: If is not true that David is fast if and only if David is a poet.
 From the fact that for all x_7, x_7 is fast or x_7 is not a poet we can infer that for all x_7, if x_7 were a poet, then x_7 is fast via universal rewriting. From the fact that for all x_7, if x_7 were a poet, then x_7 is fast we can infer that if David were a poet, then David is fast via universal instantiation. Finally, from the fact that if David were fast, then David is a poet, and that if David were a poet, then David is fast we can infer that David is fast if and only if David is a poet via biconditional introduction, which contradicts that If is not true that David is fast if and only if David is a poet. Therefore, the answer is no.