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: If Michael writes a letter, then Karen is not a taxi driver. Karen is a taxi driver. David is working. Patricia is a musician if and only if Michael is writing a letter.
Michael is not writing a letter can be inferred via the modus tollens rule. Karen is a taxi driver and David is working can be inferred via the conjunction rule. David is working and Karen is a taxi driver can be inferred via the conjunction rule. If Patricia were a musician, then Michael is writing a letter can be inferred via the biconditional elimination rule. If Michael writes a letter, then Patricia is a musician can be inferred via the biconditional elimination rule.