ANTE_CONJ_CONV : conv
STRUCTURE
SYNOPSIS
Eliminates a conjunctive antecedent in favour of implication.
DESCRIPTION
When applied to a term of the form (t1 /\ t2) ==> t, the conversion ANTE_CONJ_CONV returns the theorem:
   |- (t1 /\ t2 ==> t) = (t1 ==> t2 ==> t)

FAILURE
Fails if applied to a term not of the form "(t1 /\ t2) ==> t".
USES
Somewhat ad-hoc, but can be used (with CONV_TAC) to transform a goal of the form ?- (P /\ Q) ==> R into the subgoal ?- P ==> (Q ==> R), so that only the antecedent P is moved into the assumptions by DISCH_TAC.
SEEALSO
HOL  Kananaskis-13