EQ_MP : thm -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Equality version of the Modus Ponens rule.
DESCRIPTION
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
EQ_IMP_RULE, IMP_ANTISYM_RULE, MP
HOL  Kananaskis-13