MP : thm -> thm -> thm

SYNOPSIS
Implements the Modus Ponens inference rule.

DESCRIPTION
When applied to theorems A1 |- t1 ==> t2 and A2 |- t1, the inference rule MP returns the theorem A1 u A2 |- t2. 
    A1 |- t1 ==> t2   A2 |- t1
   ----------------------------  MP
          A1 u A2 |- t2

FAILURE CONDITIONS
Fails unless the first theorem is an implication whose antecedent is the same as the conclusion of the second theorem (up to alpha-conversion).

EXAMPLE
  # let th1 = TAUT `p ==> p \/ q`
    and th2 = ASSUME `p:bool`;;
  val th1 : thm = |- p ==> p \/ q
  val th2 : thm = p |- p

  # MP th1 th2;;
  val it : thm = p |- p \/ q

SEE ALSO
EQ_MP, MATCH_MP, MATCH_MP_TAC, MP_TAC.