# Implication in terms of biconditional and conjunction. Theorem *4.71 of
# [bib/WhiteheadRussell] p. 120 (with conjunct reversed).
Implication as a biconditional and conjunction
thm (pm4.71r () () (<-> (-> ph ps) (<-> ph (/\ ps ph))) ph ps
(<-> (-> ph ps) (<-> ph (/\ ps ph)))