EQ_MP : thm -> thm -> thm
Equality version of the Modus Ponens rule.
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'
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
# 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
This is one of HOL Light's 10 primitive inference rules.
- SEE ALSO
EQ_IMP_RULE, IMP_ANTISYM_RULE, MP, PROVE_HYP.