commuteEquivR swaps both sides of a bi-implication P↔Q to Q↔P (in the succedent).

See also