EQ_MP : thm -> thm -> thm
A1 |- t1 <=> t2 A2 |- t1 ---------------------------- EQ_MP A1 u A2 |- t2
# 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