ibar Show Code edit
# Introduction of antecedent as conjunct.
## Introduce antecedent as conjunct
thm (ibar () () (-> ph (<-> ps (/\ ph ps))) ph ps anclb pm5.74ri)
(-> ph (<-> ps (/\ ph ps)))
edit