IMP_TRANS : thm -> thm -> thm
A1 |- t1 ==> t2 A2 |- t2 ==> t3 ----------------------------------- IMP_TRANS A1 u A2 |- t1 ==> t3
# let th1 = TAUT `p /\ q /\ r ==> p /\ q` and th2 = TAUT `p /\ q ==> p`;; val th1 : thm = |- p /\ q /\ r ==> p /\ q val th2 : thm = |- p /\ q ==> p # IMP_TRANS th1 th2;; val it : thm = |- p /\ q /\ r ==> p