PROVE_HYP : thm -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Eliminates a provable assumption from a theorem.
DESCRIPTION
When applied to two theorems, PROVE_HYP returns a theorem having the conclusion of the second. The new hypotheses are the union of the two hypothesis sets (first deleting, however, the conclusion of the first theorem from the hypotheses of the second). 

     A1 |- t1     A2 |- t2
   ------------------------  PROVE_HYP
    A1 u (A2 - {t1}) |- t2

FAILURE
Never fails.
COMMENTS
This is the Cut rule. It is not necessary for the conclusion of the first theorem to be the same as an assumption of the second, but PROVE_HYP is otherwise of doubtful value.
SEEALSO
DISCH, MP, UNDISCH
HOL  Trindemossen-1