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