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