Consider the following premises. Charles is not driving a car. If Charles drives a car, then Elisabeth is happy. Charles is driving a car if and only if Elisabeth is happy. Can we infer the following from them? If we can, name the inference rule being used: Elisabeth is happy.
 From the fact that Charles is driving a car if and only if Elisabeth is happy we can infer that if Elisabeth were happy, then Charles is driving a car via biconditional elimination. From the fact that if Elisabeth were happy, then Charles is driving a car, and that if Charles drives a car, then Elisabeth is happy we can infer that Elisabeth is happy if and only if Charles is driving a car via biconditional introduction. Finally, from the fact that Elisabeth is happy if and only if Charles is driving a car, and that Charles is not driving a car we can infer that Elisabeth is not happy via biconditional elimination, which contradicts that Elisabeth is happy. Therefore, the answer is no.