The equivR proof rule proves a bi-implication P↔Q by separately assuming its left-hand side P to prove its right-hand side Q and, on a separate branch, assuming its right-hand side Q to prove its left-hand side P.

See also