PROVE_HYP : thm -> thm -> thm
A1 |- t1 A2 |- t2 ------------------------- PROVE_HYP A1 u (A2 - {t1}) |- t2
# let th1 = CONJUNCT2(ASSUME `p /\ q /\ r`) and th2 = CONJUNCT2(ASSUME `q /\ r`);; val th1 : thm = p /\ q /\ r |- q /\ r val th2 : thm = q /\ r |- r # PROVE_HYP th1 th2;; val it : thm = p /\ q /\ r |- r