IMP_CONJ : (thm -> thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Conjoins antecedents and consequents of two implications.
DESCRIPTION
When applied to theorems A1 |- p ==> r and A2 |- q ==> s, the IMP_CONJ inference rule returns the theorem A1 u A2 |- p /\ q ==> r /\ s. 
    A1 |- p ==> r    A2 |- q ==> s
   --------------------------------  IMP_CONJ
     A1 u A2 |- p /\ q ==> r /\ s

FAILURE
Fails unless the conclusions of both theorems are implicative.
SEEALSO
CONJ
HOL  Kananaskis-10