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