MK_CONJ : thm -> thm -> thm
A |- p <=> p' B |- q <=> q' ----------------------------------- MK_CONJ A u B |- p /\ q <=> p' /\ q'
# let th1 = ARITH_RULE `0 < n <=> ~(n = 0)` and th2 = ARITH_RULE `1 <= n <=> ~(n = 0)`;; val th1 : thm = |- 0 < n <=> ~(n = 0) val th2 : thm = |- 1 <= n <=> ~(n = 0) # MK_CONJ th1 th2;; val it : thm = |- 0 < n /\ 1 <= n <=> ~(n = 0) /\ ~(n = 0)