EQ_MP : thm -> thm -> thm

SYNOPSIS
Equality version of the Modus Ponens rule.

DESCRIPTION
When applied to theorems A1 |- t1 <=> t2 and A2 |- t1' where t1 and t1' are alpha-equivalent (for example, identical), the inference rule EQ_MP returns the theorem A1 u A2 |- t2.
    A1 |- t1 <=> t2   A2 |- t1'
   -----------------------------  EQ_MP
         A1 u A2 |- t2

FAILURE CONDITIONS
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.

EXAMPLE
  # let th1 = SPECL [`p:bool`; `q:bool`] CONJ_SYM
    and th2 = ASSUME `p /\ q`;;
  val th1 : thm = |- p /\ q <=> q /\ p
  val th2 : thm = p /\ q |- p /\ q
  # EQ_MP th1 th2;;
  val it : thm = p /\ q |- q /\ p

COMMENTS
This is one of HOL Light's 10 primitive inference rules.

SEE ALSO
EQ_IMP_RULE, IMP_ANTISYM_RULE, MP, PROVE_HYP.