pm5.32i Show Code edit
# Distribution of implication over biconditional (inference rule).
## Distributive Property
thm (pm5.32i () (pm5.32i.1 (-> ph (<-> ps ch))) (<-> (/\ ph ps) (/\ ph ch)) pm5.32i.1 ph ps ch pm5.32 mpbi)
(<-> (/\ ph ps) (/\ ph ch))
edit