CONJUNCT1 : thm -> thm
STRUCTURE
Thm
SYNOPSIS
Extracts left conjunct of theorem.
DESCRIPTION
    A |- t1 /\ t2
   ---------------  CONJUNCT1
       A |- t1

FAILURE
Fails unless the input theorem is a conjunction.
COMMENTS
The theorem AND1_THM can be instantiated to similar effect.
SEEALSO
BODY_CONJUNCTS, CONJUNCT2, CONJ_PAIR, CONJ, LIST_CONJ, CONJ_LIST, CONJUNCTS
HOL  Trindemossen-1