The equivL proof rule uses a bi-implication P↔Q among its assumptions byy separately assuming both P and Q or, on a separate branch, assuming both ¬P and ¬Q since, after all, both are equivalent.

See also