CONJUNCT2

Thm.CONJUNCT2 : thm -> thm

Extracts right conjunct of theorem.

    A |- t1 /\ t2
   ---------------  CONJUNCT2
       A |- t2

Failure

Fails unless the input theorem is a conjunction.

Comments

The theorem AND2_THM can be instantiated to similar effect.

See also

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