Consider the following premises. forall x_4: T_4(x_4) -> Q_1(x_4). ~T_4(e). forall x_4: Q_1(x_4) <-> T_4(x_4). Can we infer Q_1(e) from them? If possible, name the inference rules being used at each step.
 From forall x_4: Q_1(x_4) <-> T_4(x_4) we can infer forall x_4: Q_1(x_4) -> T_4(x_4) via universal biconditional elimination. From forall x_4: T_4(x_4) -> Q_1(x_4), forall x_4: Q_1(x_4) -> T_4(x_4) we can infer forall x_4: T_4(x_4) <-> Q_1(x_4) via universal biconditional introduction. From forall x_4: T_4(x_4) <-> Q_1(x_4) we can infer T_4(e) <-> Q_1(e) via universal instantiation. Finally, from T_4(e) <-> Q_1(e), ~T_4(e) we can infer ~Q_1(e) via biconditional elimination, which contradicts Q_1(e). Therefore, the answer is no.