EQ_MP : thm -> thm -> thm
Equality version of the Modus Ponens rule.
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
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.
# 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.