biimpi Show Code edit
# a.k.a. bi1i?
## Biconditional Implies Conditional
thm (biimpi () (1 (<-> ph ps)) (-> ph ps)
1 ph ps bi1 ax-mp)
(-> ph ps)
edit