Rule to convert an equivalence into twin implications.

The command format for EQUIV-IMPLICS is:

<n>EQUIV-IMPLICS D1 D2 R P D1-HYPS D2-HYPS

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

The arguments have the following meaning:

D1 : Line with Equivalence

D2 : Line with Implications in Both Directions

R : Right Equivalent

P : Left Equivalent

D1-HYPS : Hypotheses

D2-HYPS : Hypotheses

Its priority is 1

© 1988-99, Carnegie Mellon University.