Description: From a closed form theorem (the major premise) with an antecedent in the
"strong necessity" modality (in the language of modal logic), deduce the
inference |- ph => |- ps . Strong necessity is stronger than
necessity, and equivalent to it when sp (modal T) is available.
Therefore, this theorem is stronger than mpg when sp is not
available. (Contributed by BJ, 1-Nov-2023)