ancrb Show Code edit
# Conjoin antecedent to right of consequent.
## 'Add Antecedent as consequent'
thm (ancrb () () (<-> (-> ph ps) (-> ph (/\ ps ph))) ph ps ancr ps ph pm3.26 ph imim2i impbii)
(<-> (-> ph ps) (-> ph (/\ ps ph)))
edit