pm4.71r Show Code edit
# 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 pm4.71 ph ps ancom ph bibi2i bitri)
(<-> (-> ph ps) (<-> ph (/\ ps ph)))
edit