MBED-IMPLICS-RIGHT : WFFOPMBED-IMPLICS-RIGHT is a wff operation.
Embed the current edwff as the consequent of a conditional.
The antecedent is provided by the user.
The calling scheme for MBED-IMPLICS-RIGHT is:
(MBED-IMPLICS-RIGHT LGWFF RGWFF)
The result is of type GWFF0.
The arguments have the following meaning:
LGWFF : Antecedent of implication
RGWFF : Succedent of implication
TPS documentation homepage