prth Show Code edit
# Theorem *3.47 of [bib/WhiteheadRussell] p. 113.
## Praeclarum Theorema
## right('Infer', '→')
##
## This was proved by Leibniz, and it evidently pleased him enough to call it
## 'praeclarum theorema' (splendid theorem).
##
thm (prth () () (-> (/\ (-> ph ps) (-> ch th)) (-> (/\ ph ch) (/\ ps th))) ps th pm3.2 ch imim2d ph imim2i com23 imp4b)
(-> (/\ (-> ph ps) (-> ch th)) (-> (/\ ph ch) (/\ ps th)))
edit