CONJUNCT1

Thm.CONJUNCT1 : thm -> thm

Extracts left conjunct of theorem.

    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.

See also

Drule.BODY_CONJUNCTS, Thm.CONJUNCT2, Drule.CONJ_PAIR, Thm.CONJ, Drule.LIST_CONJ, Drule.CONJ_LIST, Drule.CONJUNCTS