pm5.74 Show Code edit
# Distribution of implication over biconditional. Theorem *5.74 of
# [bib/WhiteheadRussell] p. 126.
## Distributive Property
thm (pm5.74 () () (<-> (-> ph (<-> ps ch)) (<-> (-> ph ps) (-> ph ch))) ps ch bi1 ph imim3i ps ch bi2 ph imim3i impbid (-> ph ps) (-> ph ch) bi1 pm2.86d (-> ph ps) (-> ph ch) bi2 pm2.86d anim12d ph pm4.24 ps ch dfbi2 3imtr4g impbii)
(<-> (-> ph (<-> ps ch)) (<-> (-> ph ps) (-> ph ch)))
edit