biimpcd Show Code edit
# Getting a bit decadent here... just use biimpd com12!
## Biconditional Implies Conditional
thm (biimpcd () (1 (-> ph (<-> ps ch))) (-> ps (-> ph ch))
1 biimpd com12)
(-> ps (-> ph ch))
edit