What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? Name the inference rule being used: forall y_2: R_1(y_2) -> T_4(y_2). ~T_4(a_11). forall y_2: T_4(y_2) -> R_1(y_2). t.
~T_4(a_11) and t can be inferred via the conjunction rule. t and ~T_4(a_11) can be inferred via the conjunction rule. forall y_2: R_1(y_2) <-> T_4(y_2) can be inferred via the universal biconditional introduction rule. forall y_2: T_4(y_2) <-> R_1(y_2) can be inferred via the universal biconditional introduction rule.