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: Elisabeth is an astronaut. For all x, x will not play squash. Elisabeth is sad if and only if Barbara is playing squash.
If Elisabeth were sad, then Barbara is playing squash can be inferred via the biconditional elimination rule. If Barbara plays squash, then Elisabeth is sad can be inferred via the biconditional elimination rule.