Consider the following premises. For all x_10, x_10 is an astronaut if and only if x_10 will go running. For all x, x will go running. Can we infer the following from them? If we can, name the inference rule being used: Michael is an astronaut.
 From the fact that for all x_10, x_10 is an astronaut if and only if x_10 will go running we can infer that for all x_10, if x_10 goes running, then x_10 is an astronaut via universal biconditional elimination. From the fact that for all x, x will go running we can infer that Michael is running via universal instantiation. From the fact that for all x_10, if x_10 goes running, then x_10 is an astronaut we can infer that if Michael goes running, then Michael is an astronaut via universal instantiation. Finally, from the fact that if Michael goes running, then Michael is an astronaut, and that Michael is running we can infer that Michael is an astronaut via modus ponens. Therefore, the answer is yes.