pm5.32d Show Code edit
# Distribution of implication over biconditional (deduction rule).
## Distributive Property
thm (pm5.32d () (pm5.32d.1 (-> ph (-> ps (<-> ch th)))) (-> ph (<-> (/\ ps ch) (/\ ps th))) pm5.32d.1 ps ch th pm5.32 sylib)
(-> ph (<-> (/\ ps ch) (/\ ps th)))
edit