----------------------------------------------------------------------
IMP_CONJ                                                       (Drule)
----------------------------------------------------------------------
IMP_CONJ : (thm -> thm -> thm)

SYNOPSIS
Conjoins antecedents and consequents of two implications.

KEYWORDS
rule, implication, conjunction.

DESCRIBE
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
Thm.CONJ.

----------------------------------------------------------------------