anclb Show Code edit
# Conjoin antecedent to left of consequent. Theorem *4.7 of
# [bib/WhiteheadRussell] p. 120.
## 'Add Antecedent as consequent'
thm (anclb () () (<-> (-> ph ps) (-> ph (/\ ph ps))) ph ps ancl ph ps pm3.27 ph imim2i impbii)
(<-> (-> ph ps) (-> ph (/\ ph ps)))
edit