Attempt to prove a theorem directly from previously-proved theorems.
This variant of defthm<w generates a defthmd event instead of a defthm event, but otherwise is the same as defthm<w. See defthm<w.
