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.