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