Description: This theorem can be used to shorten F = hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013) (New usage is discouraged.)