Consider the following premises. David is a server or Barbara is playing tennis. If Barbara plays tennis, then David is an office clerk. For all y, y is an office clerk if and only if y is a server. Can we infer the following from them? If we can, name the inference rule being used: David is an office clerk.
 From the fact that for all y, y is an office clerk if and only if y is a server we can infer that David is an office clerk if and only if David is a server via universal instantiation. From the fact that David is an office clerk if and only if David is a server we can infer that if David were a server, then David is an office clerk via biconditional elimination. Finally, from the fact that if David were a server, then David is an office clerk, that if Barbara plays tennis, then David is an office clerk, and that David is a server or Barbara is playing tennis we can infer that David is an office clerk via disjunction elimination. Therefore, the answer is yes.