LIST_MP : thm list -> thm -> thm
STRUCTURE
SYNOPSIS
Performs a chain of Modus Ponens inferences.
DESCRIPTION
When applied to theorems A1 |- t1, ..., An |- tn and a theorem which is a chain of implications with the successive antecedents the same as the conclusions of the theorems in the list (up to alpha-conversion), A |- t1 ==> ... ==> tn ==> t, the LIST_MP inference rule performs a chain of MP inferences to deduce A u A1 u ... u An |- t.
    A1 |- t1 ... An |- tn      A |- t1 ==> ... ==> tn ==> t
   ---------------------------------------------------------  LIST_MP
                    A u A1 u ... u An |- t

FAILURE
Fails unless the theorem is a chain of implications whose consequents are the same as the conclusions of the list of theorems (up to alpha-conversion), in sequence.
SEEALSO
HOL  Trindemossen-1