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 x_23: P_23(x_23) <-> Q_23(x_23). ~w. w <-> P_23(a_19).
w -> P_23(a_19) can be inferred via the biconditional elimination rule. P_23(a_19) -> w can be inferred via the biconditional elimination rule. ~P_23(a_19) can be inferred via the biconditional elimination rule. forall x_23: P_23(x_23) -> Q_23(x_23) can be inferred via the universal biconditional elimination rule. forall x_23: Q_23(x_23) -> P_23(x_23) can be inferred via the universal biconditional elimination rule.