pm5.32 Show Code edit
# Distribution of implication over biconditional. Theorem *5.32 of
# [bib/WhiteheadRussell] p. 125.
## Distributive Property
thm (pm5.32 () () (<-> (-> ph (<-> ps ch)) (<-> (/\ ph ps) (/\ ph ch))) ps ch notbi ph imbi2i ph (-. ps) (-. ch) pm5.74 (-> ph (-. ps)) (-> ph (-. ch)) notbi 3bitri ph ps df-an ph ch df-an bibi12i bitr4i)
(<-> (-> ph (<-> ps ch)) (<-> (/\ ph ps) (/\ ph ch)))
edit