Consider the following premises. It is overcast or David is not a mechanic. If it is overcast, then Mary is sad. If Mary were sad, then David is a mechanic. Can we infer the following from them? If we can, name the inference rule being used: David is a mechanic if and only if it is overcast.
 From the fact that it is overcast or David is not a mechanic we can infer that if David were a mechanic, then it is overcast via rewriting. From the fact that if it is overcast, then Mary is sad, and that if Mary were sad, then David is a mechanic we can infer that if it is overcast, then David is a mechanic via transitivity. Finally, from the fact that if David were a mechanic, then it is overcast, and that if it is overcast, then David is a mechanic we can infer that David is a mechanic if and only if it is overcast via biconditional introduction. Therefore, the answer is yes.