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