MP is a top-level command.
Modus Ponens.
The command format for MP is:

 <n>MP   D2   D3   P1    B      A     D2-HYPS    D3-HYPS    P1-HYPS 

The arguments have the following meaning:
D2 : Line with Implication
D3 : Line with Succedent of Implication
P1 : Line with Antecedent of Implication
B : Succedent of Implication
A : Antecedent of Implication
D2-HYPS : Hypotheses
D3-HYPS : Hypotheses
P1-HYPS : Hypotheses

ETPS documentation homepage


MP is an inference rule.
Its priority is 4

ETPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage