imnan Show Code edit
## Implication in terms of conjunction
thm (imnan () () (<-> (-> ph (-. ps)) (-. (/\ ph ps)))
ph ps df-an
(<-> (/\ ph ps) (-. (-> ph (-. ps))))
con2bii
(<-> (-> ph (-. ps)) (-. (/\ ph ps)))
)
edit