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