Consider the following premises. Joseph is excited if and only if Mary is an astronaut. If Joseph were a politician, then Mary is an astronaut. For all y_4, y_4 is a politician. Can we infer the following from them? If we can, name the inference rule being used: Mary is not an astronaut.
 From the fact that for all y_4, y_4 is a politician we can infer that for all y_4, y_4 is a politician or y_4 is excited via universal addition. From the fact that for all y_4, y_4 is a politician or y_4 is excited we can infer that Joseph is a politician or Joseph is excited via universal instantiation. From the fact that Joseph is excited if and only if Mary is an astronaut we can infer that if Joseph were excited, then Mary is an astronaut via biconditional elimination. Finally, from the fact that if Joseph were a politician, then Mary is an astronaut, that if Joseph were excited, then Mary is an astronaut, and that Joseph is a politician or Joseph is excited we can infer that Mary is an astronaut via disjunction elimination, which contradicts that Mary is not an astronaut. Therefore, the answer is no.