biimpri Show Code edit
## Biconditional Implies Conditional
##
## ((<-> ph ps)) (-> ps ph))
##
thm (biimpri () (1 (<-> ph ps)) (-> ps ph)
1 ph ps bi2 ax-mp)
(-> ps ph)
edit