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