IMP_ANTISYM_RULE : thm -> thm -> thm
A1 |- t1 ==> t2 A2 |- t2 ==> t1 ------------------------------------- IMP_ANTISYM_RULE A1 u A2 |- t1 <=> t2
# let th1 = TAUT `p /\ q ==> q /\ p` and th2 = TAUT `q /\ p ==> p /\ q`;; val th1 : thm = |- p /\ q ==> q /\ p val th2 : thm = |- q /\ p ==> p /\ q # IMP_ANTISYM_RULE th1 th2;; val it : thm = |- p /\ q <=> q /\ p