pm5.1 Show Code edit
# Two propositions are equivalent if they are both true. Theorem *5.1 of
# [bib/WhiteheadRussell] p. 123.
## Two truths are equivalent
thm (pm5.1 () () (-> (/\ ph ps) (<-> ph ps)) ph ps pm5.501 biimpa)
(-> (/\ ph ps) (<-> ph ps))
edit