Description: This theorem, called "Assertion", can be thought of as closed form of
modus ponens ax-mp . Theorem *2.27 of WhiteheadRussell p. 104. Copy
of pm2.27 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018)(New usage is discouraged.)(Proof modification is discouraged.)