----------------------------------------------------------------------
EQ_MP                                                            (Thm)
----------------------------------------------------------------------
EQ_MP : thm -> thm -> thm

SYNOPSIS
Equality version of the Modus Ponens rule.

KEYWORDS
rule, equality, modus, ponens.

DESCRIBE
When applied to theorems {A1 |- t1 = t2} and {A2 |- t1}, the inference
rule {EQ_MP} returns the theorem {A1 u A2 |- t2}.

    A1 |- t1 = t2   A2 |- t1
   --------------------------  EQ_MP
         A1 u A2 |- t2




FAILURE
Fails unless the first theorem is equational and its left side
is the same as the conclusion of the second theorem (and is therefore
of type {bool}), up to alpha-conversion.

SEEALSO
Thm.EQ_IMP_RULE, Drule.IMP_ANTISYM_RULE, Thm.MP.

----------------------------------------------------------------------