Biconditional elimination

In symbolic logic, a valid inference in a system of truth-functional rules. The affirmation of one side of the biconditional yields the other.