Rule to convert twin implications into an equivalence.

The command format for IMPLICS-EQUIV is:

<n>IMPLICS-EQUIV P2 P1 R P P2-HYPS P1-HYPS

"LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST"

The arguments have the following meaning:

P2 : Line with Equivalence

P1 : Line with Implications in Both Directions

R : Right Equivalent

P : Left Equivalent

P2-HYPS : Hypotheses

P1-HYPS : Hypotheses

Its priority is 1

© 1988-99, Carnegie Mellon University.