biimprd Show Code edit
## Biconditional Implies Conditional
thm (biimprd () (1 (-> ph (<-> ps ch))) (-> ph (-> ch ps))
1 ps ch bi2 syl)
(-> ph (-> ch ps))
edit