abai Show Code edit
## Introduce conjunct as antecedent
## left('Simplify', '→')
thm (abai () () (<-> (/\ ph ps) (/\ ph (-> ph ps))) ph ps pm3.26 ph ps pm3.4 jca ph (-> ph ps) pm3.26 ph ps pm3.35 jca impbii)
(<-> (/\ ph ps) (/\ ph (-> ph ps)))
edit