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