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: p_8 <-> T(e_1). forall x: ~T(x). q.
p_8 -> T(e_1) can be inferred via the biconditional elimination rule. T(e_1) -> p_8 can be inferred via the biconditional elimination rule.