CONJ

Thm.CONJ : thm -> thm -> thm

Introduces a conjunction.

    A1 |- t1      A2 |- t2
   ------------------------  CONJ
     A1 u A2 |- t1 /\ t2

Failure

Never fails.

Comments

The theorem AND_INTRO_THM can be instantiated to similar effect.

See also

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